A linear-time model-checking algorithm for the alternation-free modal mu- calculus
From MaRDI portal
Publication:1801498
DOI10.1007/BF01383878zbMath0772.68038MaRDI 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
automated verification; automated verification tools for finite-state processes; model-checking algorithms
68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03B45: Modal logic (including the logic of norms)
Related Items
Local model checking for context-free processes, Efficient local correctness checking for single and alternating boolean equation systems, An even faster solver for general systems of equations, Data flow analysis as model checking, Generating diagnostic information for behavioral preorders, Alternating automata: Unifying truth and validity checking for temporal logics, On model checking for the \(\mu\)-calculus and its fragments, Alternation-free weighted mu-calculus: decidability and completeness, Unnamed Item, Improved model checking of hierarchical systems, Symbolic bounded synthesis, The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity, Maximally permissive controlled system synthesis for non-determinism and modal logic, CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks, Regular languages of nested words: fixed points, automata, and synchronization, Model checking for hybrid logic, Model checking and boolean graphs, Model checking for action-based logics, Fast and simple nested fixpoints, Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL, On decidability of recursive weighted logics, Module checking, Is your model checker on time? On the complexity of model checking for timed modal logics, Complete proof systems for weighted modal logic, Compositional verification of asynchronous concurrent systems using CADP, On the universal and existential fragments of the \(\mu\)-calculus, Compositional analysis for verification of parameterized systems, Model checking hybrid logics (with an application to semistructured data), Probabilistic temporal logics via the modal mu-calculus, Characteristic Formulae for Timed Automata, Local Model Checking in a Logic for True Concurrency, The mu-calculus and Model Checking, Computation Tree Regular Logic for Genetic Regulatory Networks, Inf-datalog, Modal Logic and Complexities, Solving μ-Calculus Parity Games by Symbolic Planning, Logical Foundations of XML and XQuery
Cites Work
- 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
- Unnamed Item
- Unnamed Item
