### Abstract

This entry provides a formalization of the abstract theory of ample set partial order reduction. The formalization includes transition systems with actions, trace theory, as well as basics on finite, infinite, and lazy sequences. We also provide a basic framework for static analysis on concurrent systems with respect to the ample set condition.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Partial_Order_Reduction

- List_Prefixes
- List_Extensions
- Word_Prefixes
- Set_Extensions
- Basic_Extensions
- Relation_Extensions
- Transition_System_Extensions
- Traces
- Transition_System_Traces
- Functions
- ENat_Extensions
- CCPO_Extensions
- ESet_Extensions
- Coinductive_List_Extensions
- LList_Prefixes
- Stuttering
- Transition_System_Interpreted_Traces
- Ample_Abstract
- Formula
- Ample_Correctness
- Ample_Analysis

### Depends on

- Coinductive
- Stuttering Equivalence
- Transition Systems and Automata

### Used by

- A Fully Verified Executable LTL Model Checker

## Cite

×

Partial_Order_Reduction-AFP

    @article{Partial_Order_Reduction-AFP,
      author  = {Julian Brunner},
      title   = {Partial Order Reduction},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Partial_Order_Reduction.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018