Email Gateway (Jun 21 2023 at 05:41): Email Gateway (Jun 21 2023 at 05:41):From: Gerwin Klein <kleing@unsw.edu.au>
DCR Syntax and Execution Equivalent Markings
by Axel Christfort and Søren Debois
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.
https://www.isa-afp.org/entries/DCR-ExecutionEquivalence.html
Enjoy!
Gerwin
Last updated: Jan 04 2025 at 20:18 UTC