Tableau-based model checking in the propositional mu-calculus
This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.
- Model checking for hybrid logic
- Local model checking in the modal mu-calculus
- Local model checking for infinite state spaces
- Reasoning about nondeterministic and concurrent actions: A process algebra approach
- A compositional -calculus proof system for statecharts processes
- Model checking and boolean graphs
- CTL^* and ECTL^* as fragments of the modal -calculus
- Proving properties of dynamic process networks
- A graphical \(\mu\)-calculus and local model checking.
- A local approach for temporal model checking of Java bytecode
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- A new logic for electronic commerce protocols
- Selective mu-calculus and formula-based equivalence of transition systems
- Program schemata technique for propositional program logics: a 30-year history
- Bounded model checking of infinite state systems
- The alternation hierarchy in fixpoint logic with chop is strict too
- Probabilistic temporal logics via the modal mu-calculus
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- Tableaux for verification of data-centric processes
- Minimal Proof Search for Modal Logic K Model Checking
- scientific article; zbMATH DE number 2186291 (Why is no real title available?)
- The mu-calculus and Model Checking
- Tableaux and model checking for memory logics
- A tableau system for the modal -calculus
- Solving parity games by a reduction to SAT
- scientific article; zbMATH DE number 516989 (Why is no real title available?)
- scientific article; zbMATH DE number 1059247 (Why is no real title available?)
- scientific article; zbMATH DE number 1499079 (Why is no real title available?)
- scientific article; zbMATH DE number 1790379 (Why is no real title available?)
- scientific article; zbMATH DE number 1796122 (Why is no real title available?)
- Proving correctness of labeled transition systems by semantic tableaux
- Tableau methods for PA-processes
- Local model checking for context-free processes
- Efficient local correctness checking for single and alternating boolean equation systems
- scientific article; zbMATH DE number 2102740 (Why is no real title available?)
- An on-the-fly tableau-based decision procedure for PDL-satisfiability
- A proof theory for model checking: an extended abstract
- Three notes on the complexity of model checking fixpoint logic with chop
- On model checking for the -calculus and its fragments
- A game-theoretic framework for specification and verification of cryptographic protocols
- Compositional checking of satisfaction
- Modular abstractions for verifying real-time distributed systems
- Compositional checking of satisfaction
- The expressive power of implicit specifications
- Compositionality and locality for improving model checking in the selective mu-calculus
- Distributed symbolic model checking for -calculus
- Reduced models for efficient CCS verification
This page was built for publication: Tableau-based model checking in the propositional mu-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1122572)
