Tableau-based model checking in the propositional mu-calculus
From MaRDI portal
Recommendations
Cited in
(46)- Proving properties of dynamic process networks
- Compositional checking of satisfaction
- Modular abstractions for verifying real-time distributed systems
- The expressive power of implicit specifications
- Reasoning about nondeterministic and concurrent actions: A process algebra approach
- Program schemata technique for propositional program logics: a 30-year history
- Three notes on the complexity of model checking fixpoint logic with chop
- Solving parity games by a reduction to SAT
- Compositionality and locality for improving model checking in the selective mu-calculus
- scientific article; zbMATH DE number 1059247 (Why is no real title available?)
- An on-the-fly tableau-based decision procedure for PDL-satisfiability
- Minimal Proof Search for Modal Logic K Model Checking
- A graphical \(\mu\)-calculus and local model checking.
- Local model checking in the modal mu-calculus
- A tableau system for the modal \(\mu \)-calculus
- CTL^* and ECTL^* as fragments of the modal -calculus
- A compositional -calculus proof system for statecharts processes
- A game-theoretic framework for specification and verification of cryptographic protocols
- Tableau methods for PA-processes
- A local approach for temporal model checking of Java bytecode
- On model checking for the \(\mu\)-calculus and its fragments
- scientific article; zbMATH DE number 516989 (Why is no real title available?)
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- The mu-calculus and Model Checking
- Model checking and boolean graphs
- Probabilistic temporal logics via the modal mu-calculus
- Local model checking for infinite state spaces
- Selective mu-calculus and formula-based equivalence of transition systems
- Tableaux for verification of data-centric processes
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- A proof theory for model checking: an extended abstract
- scientific article; zbMATH DE number 2186291 (Why is no real title available?)
- Compositional checking of satisfaction
- The alternation hierarchy in fixpoint logic with chop is strict too
- Model checking for hybrid logic
- Proving correctness of labeled transition systems by semantic tableaux
- A new logic for electronic commerce protocols
- scientific article; zbMATH DE number 1796122 (Why is no real title available?)
- Local model checking for context-free processes
- scientific article; zbMATH DE number 1790379 (Why is no real title available?)
- Distributed symbolic model checking for \(\mu\)-calculus
- Reduced models for efficient CCS verification
- Tableaux and model checking for memory logics
- Efficient local correctness checking for single and alternating boolean equation systems
- scientific article; zbMATH DE number 2102740 (Why is no real title available?)
- Bounded model checking of infinite state systems
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)
