From Dynamic Condition Response Structures to Büchi Automata

TY - GEN

T1 - From Dynamic Condition Response Structures to Büchi Automata

AU - Mukkamala, Raghava Rao

AU - Hildebrandt, Thomas

N1 - @article{10.1109/TASE.2010.22, author = {Raghava Rao Mukkamala and Thomas T. Hildebrandt}, title = {From Dynamic Condition Response Structures to Buchi Automata}, journal ={Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on}, volume = {0}, isbn = {978-0-7695-4148-8}, year = {2010}, pages = {187-190}, doi = {http://doi.ieeecomputersociety.org/10.1109/TASE.2010.22}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

PY - 2010

Y1 - 2010

N2 - 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 Büchi-automata. This is the first step towards automatic verification of processes specified as DCR structures.

AB - 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 Büchi-automata. This is the first step towards automatic verification of processes specified as DCR structures.

U2 - 10.1109/tase.2010.22

DO - 10.1109/tase.2010.22

M3 - Article in proceedings

SN - 978-0-7695-4148-8

VL - 0

SP - 187

EP - 190

BT - From Dynamic Condition Response Structures to Büchi Automata

PB - IEEE Computer Society Press

ER -