DCR Syntax and Execution Equivalent Markings

Axel Christfort 📧 and Søren Debois

June 16, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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