A linear-time model-checking algorithm for the alternation-free modal mu- calculus
From MaRDI portal
Recommendations
Cites work
- A lattice-theoretical fixpoint theorem and its applications
- A linear algorithm to solve fixed-point equations on transition systems
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Computing behavioural relations, logically
- scientific article; zbMATH DE number 4056971 (Why is no real title available?)
- Propositional dynamic logic of regular programs
- Results on the propositional \(\mu\)-calculus
- Tableau-based model checking in the propositional mu-calculus
Cited in
(50)- 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
- Local model checking and protocol analysis
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Efficient on-the-fly model-checking for regular alternation-free -calculus
- 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 autoamta
- Parallel model checking for the alternation free -calculus
- Alternating context-free languages and linear time -calculus with sequential composition
- Using assumptions to distribute alternation free {\(\mu\)}-calculus model checking
- Local model checking in a logic for true concurrency
- scientific article; zbMATH DE number 4131643 (Why is no real title available?)
- The mu-calculus and Model Checking
- Computation Tree Regular Logic for Genetic Regulatory Networks
- Practical Efficient Modular Linear-Time Model-Checking
- Inf-datalog, Modal Logic and Complexities
- Solving μ-Calculus Parity Games by Symbolic Planning
- Logical Foundations of XML and XQuery
- Improved model checking of hierarchical systems
- scientific article; zbMATH DE number 2080055 (Why is no real title available?)
- Symbolic bounded synthesis
- Model checking the full modal mu-calculus for infinite sequential processes
- Local model checking for context-free processes
- Efficient local correctness checking for single and alternating boolean equation systems
- The \(\mu\)-calculus alternation hierarchy collapses over structures with restricted connectivity
- An even faster solver for general systems of equations
- Data flow analysis as model checking
- Maximally permissive controlled system synthesis for non-determinism and modal logic
- Generating diagnostic information for behavioral preorders
- Alternating automata: unifying truth and validity checking for temporal logics
- From linear time to branching time
- STACS 2004
- CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
- On model checking for the -calculus and its fragments
- Alternation-free weighted mu-calculus: decidability and completeness
- Jumping evaluation of nested regular path queries
- Regular languages of nested words: fixed points, automata, and synchronization
- Automated temporal reasoning about reactive systems
- Operations on fixpoint equation systems
- Alternating-time temporal logic
This page was built for publication: A linear-time model-checking algorithm for the alternation-free modal mu- calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1801498)
