@article{Debois2017,
    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 {\$}{\$}^{\backslash}star {\$}{\$} ⋆ process language, which supports modular specification through a compositional operational semantics. DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ 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 {\$}{\$}^{\backslash}star {\$}{\$} ⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an {\$}{\$}{\backslash}omega {\$}{\$} $\omega$ -regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ language is available at http://dcr.tools/acta16 .},
    Author = {Debois, S{\o}ren and Hildebrandt, Thomas T. and Slaats, Tijs},
    ISSN = {1432-0525},
    Journal = {Acta Informatica},
    Month = {Sep},
    Title = {Replication, refinement {\&} reachability: complexity in dynamic condition-response graphs},
    URL = {https://doi.org/10.1007/s00236-017-0303-8},
    Year = {2017},
    bdsk-url-1 = {https://doi.org/10.1007/s00236-017-0303-8},
    bdsk-url-2 = {http://dx.doi.org/10.1007/s00236-017-0303-8},
    date-added = {2017-09-26 08:54:48 +0000},
    date-modified = {2017-09-26 08:54:48 +0000},
    day = {21},
    doi = {10.1007/s00236-017-0303-8}
}

@article{Debois2017, 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 {\$}{\$}^{\backslash}star {\$}{\$} ⋆ process language, which supports modular specification through a compositional operational semantics. DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ 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 {\$}{\$}^{\backslash}star {\$}{\$} ⋆ processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an {\$}{\$}{\backslash}omega {\$}{\$} $\omega$ -regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR {\$}{\$}^{\backslash}star {\$}{\$} ⋆ language is available at http://dcr.tools/acta16 .}, Author = {Debois, S{\o}ren and Hildebrandt, Thomas T. and Slaats, Tijs}, ISSN = {1432-0525}, Journal = {Acta Informatica}, Month = {Sep}, Title = {Replication, refinement {\&} reachability: complexity in dynamic condition-response graphs}, URL = {https://doi.org/10.1007/s00236-017-0303-8}, Year = {2017}, bdsk-url-1 = {https://doi.org/10.1007/s00236-017-0303-8}, bdsk-url-2 = {http://dx.doi.org/10.1007/s00236-017-0303-8}, date-added = {2017-09-26 08:54:48 +0000}, date-modified = {2017-09-26 08:54:48 +0000}, day = {21}, doi = {10.1007/s00236-017-0303-8} }