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


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
PublisherIEEE Computer Society Press
Publication date2010
ISBN (Print)978-0-7695-4148-8
Publication statusPublished - 2010


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


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

Cite this