From Dynamic Condition Response Structures to Büchi Automata

Raghava Rao Mukkamala; Thomas Hildebrandt

doi:10.1109/TASE.2010.22

From Dynamic Condition Response Structures to Büchi Automata

Raghava Rao Mukkamala, Thomas Hildebrandt

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 language	English
Title of host publication	From Dynamic Condition Response Structures to Büchi Automata
Number of pages	4
Volume	0
Publisher	IEEE
Publication date	2010
Pages	187-190
ISBN (Print)	978-0-7695-4148-8
DOIs	https://doi.org/10.1109/TASE.2010.22
Publication status	Published - 2010

Keywords

Distributed Dynamic Condition Response Structures
Declarative Process Models
Causality and Conflict Dual Relations
Infinite Behavior
Büchi Automata

Access to Document

10.1109/TASE.2010.22

dcrs-buchi.pdfSubmitted manuscript, 220 KB

http://www.itu.dk/people/rao/pubs_accepted/dcrsextendedabstractTase2010.pdf

TRUSTCARE: Trustworthy Pervasive Healthcare Services
Hildebrandt, T. (PI), Bardram, J. (CoI), Mukkamala, R. R. (CoI) & Bunde-Pedersen, J. (CoI)
Danish Council for Strategic Research
01/01/2008 → 30/06/2012
Project: Research

Cite this

@inproceedings{2fa342745eaf407886d58c8084850e68,

title = "From Dynamic Condition Response Structures to B{\"u}chi Automata",

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.",

keywords = "Distributed Dynamic Condition Response Structures, Declarative Process Models, Causality and Conflict Dual Relations, Infinite Behavior, B{\"u}chi Automata, Distributed Dynamic Condition Response Structures, Declarative Process Models, Causality and Conflict Dual Relations, Infinite Behavior, B{\"u}chi Automata",

author = "Mukkamala, {Raghava Rao} and Thomas Hildebrandt",

note = "@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}, } ",

year = "2010",

doi = "10.1109/TASE.2010.22",

language = "English",

isbn = "978-0-7695-4148-8",

volume = "0",

pages = "187--190",

booktitle = "From Dynamic Condition Response Structures to B{\"u}chi Automata",

publisher = "IEEE",

address = "United States",

}

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

KW - Distributed Dynamic Condition Response Structures

KW - Declarative Process Models

KW - Causality and Conflict Dual Relations

KW - Infinite Behavior

KW - Büchi Automata

KW - Distributed Dynamic Condition Response Structures

KW - Declarative Process Models

KW - Causality and Conflict Dual Relations

KW - Infinite Behavior

KW - Büchi Automata

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

ER -

From Dynamic Condition Response Structures to Büchi Automata

Abstract

Keywords

Access to Document

Fingerprint

Projects

TRUSTCARE: Trustworthy Pervasive Healthcare Services

Cite this