From Dynamic Condition Response Structures to Büchi Automata

Raghava Rao Mukkamala, Thomas Hildebrandt

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Abstract

Recently we have presented distributed dynamic condition response structures (DCR structures) as a declarative process model conservatively generalizing labelled event structures to allow for finite specifications of repeated, possibly infinite behavior. The key ideas are to split the causality relation of event structures in two dual relations: the condition relation and the response relation, to split the conflict relation in two relations: the dynamic exclusion and dynamic inclusion, and finally to allow configurations to be multi sets of events. In the present abstract we recall the model and show how to characterise the execution of DCR structures and the acceptance condition for infinite runs by giving a map to Bu ̈chi-automata. This is the first step towards automatic verification of processes specified as DCR structures.
Original languageEnglish
Title of host publicationFrom Dynamic Condition Response Structures to Büchi Automata
Number of pages4
Volume0
PublisherIEEE Computer Society Press
Publication date2010
Pages187-190
ISBN (Print)978-0-7695-4148-8
DOIs
Publication statusPublished - 2010

Keywords

  • Distributed Dynamic Condition Response Structures
  • Declarative Process Models
  • Causality and Conflict Dual Relations
  • Infinite Behavior
  • Büchi Automata

Fingerprint

Dive into the research topics of 'From Dynamic Condition Response Structures to Büchi Automata'. Together they form a unique fingerprint.

Cite this