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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	From Dynamic Condition Response Structures to Büchi Automata
Antal sider	4
Vol/bind	0
Forlag	IEEE
Publikationsdato	2010
Sider	187-190
ISBN (Trykt)	978-0-7695-4148-8
DOI	https://doi.org/10.1109/TASE.2010.22
Status	Udgivet - 2010

Emneord

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

Adgang til dokumentet

10.1109/TASE.2010.22

dcrs-buchi.pdfIndsendt manuskript, 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
Projekter: Projekt › Forskning

Citationsformater

@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

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

TRUSTCARE: Trustworthy Pervasive Healthcare Services

Citationsformater