Partial-order methods for model checking: from linear time to branching time
- 24 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Partial-order methods make it possible to check properties of a concurrent system by state-space exploration without considering all interleavings of independent concurrent events. They have been applied to linear-time model checking, but so far only limited results are known about their applicability to branching-time model checking. In this paper, we introduce a general technique for lifting partial-order methods from linear-time to branching-time logics. This technique is shown to be applicable both to reductions that are applied to the structure representing the program before running the model checking procedure, as well as to reductions that can be obtained when model checking is done in an automata-theoretic framework. The latter are extended to branching-time logics by using the model-checking framework based on alternating automata introduced by Bernholtz, Vardi and Wolper.Keywords
This publication has 16 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- A partial order approach to branching time logic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Partial Approach to Model CheckingInformation and Computation, 1994
- A linear local model checking algorithm for CTLPublished by Springer Nature ,1993
- Partial-order methods for temporal verificationPublished by Springer Nature ,1993
- Symbolic Boolean manipulation with ordered binary-decision diagramsACM Computing Surveys, 1992
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automata-theoretic techniques for modal logics of programsJournal of Computer and System Sciences, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Checking that finite state concurrent programs satisfy their linear specificationPublished by Association for Computing Machinery (ACM) ,1985