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