A linear-time model-checking algorithm for the alternation-free modal mu- calculus

DOI10.1007/BF01383878zbMath0772.68038OpenAlexW1791618115MaRDI QIDQ1801498

Rance Cleaveland, Bernhard Steffen

Publication date: 17 August 1993

Published in: Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

automated verificationautomated verification tools for finite-state processesmodel-checking algorithms

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Modal logic (including the logic of norms) (03B45)

Related Items (36)

Model checking and boolean graphs ⋮ Model checking for action-based logics ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Compositional analysis for verification of parameterized systems ⋮ The mu-calculus and Model Checking ⋮ Fast and simple nested fixpoints ⋮ Data flow analysis as model checking ⋮ Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL ⋮ Improved model checking of hierarchical systems ⋮ Symbolic bounded synthesis ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Unnamed Item ⋮ Regular languages of nested words: fixed points, automata, and synchronization ⋮ Local Model Checking in a Logic for True Concurrency ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ Generating diagnostic information for behavioral preorders ⋮ The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity ⋮ Local model checking for context-free processes ⋮ Efficient local correctness checking for single and alternating boolean equation systems ⋮ Inf-datalog, Modal Logic and Complexities ⋮ Characteristic Formulae for Timed Automata ⋮ Maximally permissive controlled system synthesis for non-determinism and modal logic ⋮ Complete proof systems for weighted modal logic ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ On model checking for the \(\mu\)-calculus and its fragments ⋮ Model checking hybrid logics (with an application to semistructured data) ⋮ Solving μ-Calculus Parity Games by Symbolic Planning ⋮ On decidability of recursive weighted logics ⋮ Logical Foundations of XML and XQuery ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Model checking for hybrid logic ⋮ Module checking ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ An even faster solver for general systems of equations

Cites Work

• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• A linear algorithm to solve fixed-point equations on transition systems
• Tableau-based model checking in the propositional mu-calculus
• Propositional dynamic logic of regular programs
• A lattice-theoretical fixpoint theorem and its applications
• Automatic verification of finite-state concurrent systems using temporal logic specifications

This page was built for publication: A linear-time model-checking algorithm for the alternation-free modal mu- calculus