### 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

- Computer science/System description languages

### Session DCR-ExecutionEquivalence

- DCRExecutionEquivalence

## Cite

×

DCR-ExecutionEquivalence-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Jun 21, 2023 : Isabelle2022