Tableau-based model checking in the propositional mu-calculus

DOI10.1007/BF00264284zbMath0676.03033OpenAlexW2057260173MaRDI QIDQ1122572

Rance Cleaveland

Publication date: 1990

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00264284

zbMATH Keywords

propositional mu-calculusautomated analysis of concurrent systemsfinite-state systemstableau-based proof system

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Structure of proofs (03F07)

Related Items (30)

Model checking and boolean graphs ⋮ CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Bounded model checking of infinite state systems ⋮ Minimal Proof Search for Modal Logic K Model Checking ⋮ When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus ⋮ Proving properties of dynamic process networks ⋮ A game-theoretic framework for specification and verification of cryptographic protocols ⋮ Solving parity games by a reduction to SAT ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ Selective mu-calculus and formula-based equivalence of transition systems ⋮ A graphical \(\mu\)-calculus and local model checking. ⋮ Local model checking for context-free processes ⋮ Local model checking in the modal mu-calculus ⋮ Efficient local correctness checking for single and alternating boolean equation systems ⋮ Modular abstractions for verifying real-time distributed systems ⋮ Compositional checking of satisfaction ⋮ The expressive power of implicit specifications ⋮ On model checking for the \(\mu\)-calculus and its fragments ⋮ A local approach for temporal model checking of Java bytecode ⋮ Three notes on the complexity of model checking fixpoint logic with chop ⋮ The alternation hierarchy in fixpoint logic with chop is strict too ⋮ A linear-time model-checking algorithm for the alternation-free modal mu- calculus ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ A compositional \(\mu\)-calculus proof system for statecharts processes ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Model checking for hybrid logic ⋮ A new logic for electronic commerce protocols ⋮ Distributed symbolic model checking for \(\mu\)-calculus ⋮ Reduced models for efficient CCS verification

This page was built for publication: Tableau-based model checking in the propositional mu-calculus