Replication, refinement & reachability: complexity in dynamic condition-response graphs

Søren Debois; Thomas T. Hildebrandt; Tijs Slaats

doi:10.1007/s00236-017-0303-8

Replication, refinement & reachability: complexity in dynamic condition-response graphs

Søren Debois, Thomas T. Hildebrandt, Tijs Slaats

8 Citations (Scopus)

Abstract

We explore the complexity of reachability and run-time refinement under safety and liveness constraints in event-based process models. Our study is framed in the DCR^⋆ process language, which supports modular specification through a compositional operational semantics. DCR^⋆ encompasses the “Dynamic Condition Response (DCR) graphs” declarative process model for analysis, execution and safe run-time refinement of process-aware information systems; including replication of sub-processes. We prove that event-reachability and refinement are np-hard for DCR^⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an ω-regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR^⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR^⋆ language is available at http://dcr.tools/acta16.

Original language	English
Journal	Acta Informatica
Volume	55
Pages (from-to)	489–520
ISSN	0001-5903
DOIs	https://doi.org/10.1007/s00236-017-0303-8
Publication status	Published - 1 Sept 2018

Access to Document

10.1007/s00236-017-0303-8

Cite this

@article{1de1ddf4e71c46ddb65b94ee35dd61f1,

title = "Replication, refinement & reachability: complexity in dynamic condition-response graphs",

abstract = "We explore the complexity of reachability and run-time refinement under safety and liveness constraints in event-based process models. Our study is framed in the DCR⋆ process language, which supports modular specification through a compositional operational semantics. DCR⋆ encompasses the “Dynamic Condition Response (DCR) graphs” declarative process model for analysis, execution and safe run-time refinement of process-aware information systems; including replication of sub-processes. We prove that event-reachability and refinement are np-hard for DCR⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an ω-regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR⋆ language is available at http://dcr.tools/acta16.",

author = "S{\o}ren Debois and Hildebrandt, {Thomas T.} and Tijs Slaats",

year = "2018",

month = sep,

day = "1",

doi = "10.1007/s00236-017-0303-8",

language = "English",

volume = "55",

pages = "489–520",

journal = "Acta Informatica",

issn = "0001-5903",

publisher = "Springer",

}

TY - JOUR

T1 - Replication, refinement & reachability

T2 - complexity in dynamic condition-response graphs

AU - Debois, Søren

AU - Hildebrandt, Thomas T.

AU - Slaats, Tijs

PY - 2018/9/1

Y1 - 2018/9/1

N2 - We explore the complexity of reachability and run-time refinement under safety and liveness constraints in event-based process models. Our study is framed in the DCR⋆ process language, which supports modular specification through a compositional operational semantics. DCR⋆ encompasses the “Dynamic Condition Response (DCR) graphs” declarative process model for analysis, execution and safe run-time refinement of process-aware information systems; including replication of sub-processes. We prove that event-reachability and refinement are np-hard for DCR⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an ω-regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR⋆ language is available at http://dcr.tools/acta16.

AB - We explore the complexity of reachability and run-time refinement under safety and liveness constraints in event-based process models. Our study is framed in the DCR⋆ process language, which supports modular specification through a compositional operational semantics. DCR⋆ encompasses the “Dynamic Condition Response (DCR) graphs” declarative process model for analysis, execution and safe run-time refinement of process-aware information systems; including replication of sub-processes. We prove that event-reachability and refinement are np-hard for DCR⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an ω-regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR⋆ language is available at http://dcr.tools/acta16.

U2 - 10.1007/s00236-017-0303-8

DO - 10.1007/s00236-017-0303-8

M3 - Journal article

SN - 0001-5903

VL - 55

SP - 489

EP - 520

JO - Acta Informatica

JF - Acta Informatica

ER -

Replication, refinement & reachability: complexity in dynamic condition-response graphs

Abstract

Access to Document

Fingerprint

Cite this