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 eventreachability 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
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 eventreachability 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 |
Pages (from-to) | 1-32 |
Number of pages | 32 |
ISSN | 0001-5903 |
DOIs | |
Publication status | Published - 21 Sept 2017 |
Keywords
- DCR graphs
- replication
- refinement
- complexity