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.

Abstract

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.

License

BSD License

Topics

Session DCR-ExecutionEquivalence

Cite

× 
@article{DCR-ExecutionEquivalence-AFP,
  author  = {Axel Christfort and Søren Debois},
  title   = {DCR Syntax and Execution Equivalent Markings},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/DCR-ExecutionEquivalence.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: