DCR Syntax and Execution Equivalent Markings

Axel Christfort 📧 and Søren Debois

June 16, 2023


We present an Isabelle formalization of the basics of Dynamic Condition Response (DCR) graphs before defining Execution Equivalent markings. We then prove that execution equivalent markings are perfectly interchangeable during process execution, yielding significant state-space reduction for execution-based model-checking of DCR graphs.


BSD License


Session DCR-ExecutionEquivalence