Transparent partial order reduction
Partial order reduction is a technique used to tackle the state space explosion problem incurring in the verification of multi-component systems. In the interleaving semantics of parallel composition, the parallel execution of two actions from different components yields two different orders of executions in the combined system. In general, the number of different executions is exponential in the number of components. Partial order reduction identifies combinations of actions from different components that are independent of each other in the sense that considering only one particular order of execution between them does not violate the underlying correctness property. The success of partial order reductions hinges on how effective the process of deciding which actions are independent of each other is. Research in partial order reduction therefore has to provide methods that guarantee non-violence of correctness properties for particular classes of such properties, for instance those that can be defined by stutter-free LTL formulas. The paper at hand relaxes a well-known so-called invisibility condition which requires the value of no atomic proposition to be changed in transitions whose actions can be considered for partial order reductions. It shows that it is sufficient to require the values of atomic propositions never to change from positive to negative in such transitions for as long as the proposition is only used negatively in the correctness property (and vice-versa). The paper presents the theoretical foundations of this approach and reports some experimental data which show that using the weaker condition can result in stronger partial order reductions.
- Partial order reduction for checking LTL formulae with the next-time operator
- A partial order approach to branching time logic model checking.
- scientific article; zbMATH DE number 1507206
- Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
- scientific article; zbMATH DE number 1497783
- A stubborn attack on state explosion
- Combining partial-order reductions with on-the-fly model-checking.
- Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
- scientific article; zbMATH DE number 1973991 (Why is no real title available?)
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Question-guided stubborn set methods for state properties
- Relaxed visibility enhances partial order reduction
- Verification, Model Checking, and Abstract Interpretation
- An efficient partial order reduction algorithm with an alternative proviso implementation
- State space reduction using partial order techniques
- Approximate partial order reduction
- Partial order reduction for rewriting semantics of programming languages
- State space reduction for sensor networks using two-level partial order reduction
- Partial order reduction for checking LTL formulae with the next-time operator
- Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
- scientific article; zbMATH DE number 1497783 (Why is no real title available?)
- scientific article; zbMATH DE number 1538051 (Why is no real title available?)
- Partial-order reduction for parity games with an application on parameterised Boolean equation systems
- Peephole Partial Order Reduction
- Partial order reduction for state/event LTL with application to component-interaction automata
- Partial-order reduction in symbolic state-space exploration
- Relaxed visibility enhances partial order reduction
- Formal verification of an executable LTL model checker with partial order reduction
This page was built for publication: Transparent partial order reduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q453518)
