Local model checking in the modal mu-calculus
From MaRDI portal
The modal mu-calculus introduced by Pratt and Kozen is an extension of dynamic logic towards temporal logic. Formulae of the mu-calculus when interpreted on labelled transition systems may be used for modelling concurrency. For a given finite model (transition system) the problem of satisfiability is solvable. The authors present a method which is a tableau system for testing whether or not a state \(s\) has the property expressed by a formula of mu-calculus in a finite model. A nice example of an application of the method is also provided (an analysis of Knuth's mutual exclusion algorithm).
Recommendations
Cites work
- A modal characterization of observational congruence on finite terms of CCS
- A refinement calculus for specifications in Hennessy-Milner logic with recursion
- Algebraic laws for nondeterminism and concurrency
- Automated analysis of mutual exclusion algorithms using CCS
- scientific article; zbMATH DE number 4131643 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 4119603 (Why is no real title available?)
- Modal logics for communicating systems
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- Results on the propositional \(\mu\)-calculus
- Tableau-based model checking in the propositional mu-calculus
Cited in
(68)- Model checking for hybrid logic
- Tableau-based model checking in the propositional mu-calculus
- A note on model checking the modal \(\nu\)-calculus
- Local model checking for infinite state spaces
- Symbolic model checking: \(10^{20}\) states and beyond
- 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
- Axiomatising extended computation tree logic
- Petri nets, traces, and local model checking
- A graphical -calculus and local model checking.
- Local soundness for QBF calculi
- A local approach for temporal model checking of Java bytecode
- Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- On the formalization of the modal -calculus in the calculus of inductive constructions
- Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
- Discrete tense logic with infinitary inference rules and systematic frame constants: A Hilbert-style axiomatization
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Mu-calculus satisfiability with arithmetic constraints
- Bounded model checking of infinite state systems
- On complexity of verification of interacting agents' behavior
- Quantification over sets of possible worlds in branching-time semantics
- Using heuristic search for finding deadlocks in concurrent systems
- Modal logics and mu-calculi: An introduction
- Local model checking in a logic for true concurrency
- Two ways to common knowledge
- Model-Checking First-Order Logic: Automata and Locality
- Multi-valued model checking games
- scientific article; zbMATH DE number 516989 (Why is no real title available?)
- scientific article; zbMATH DE number 1059247 (Why is no real title available?)
- On global induction mechanisms in aμ-calculus with explicit approximations
- Local model-checking of modal mu-calculus on acyclic labeled transition systems
- On model checking infinite-state systems
- Model checking the full modal mu-calculus for infinite sequential processes
- Tableaux and algorithms for Propositional Dynamic Logic with Converse
- Model checking modal transition systems using Kripke structures
- An effective tableau system for the linear time -calculus
- A Note on Negative Tagging for Least Fixed-Point Formulae
- scientific article; zbMATH DE number 1432245 (Why is no real title available?)
- Polynomial-time under-approximation of winning regions in parity games
- Petri nets, traces, and local model checking
- The Recursion Scheme from the Cofree Recursive Comonad
- Formal verification of concurrent systems via directed model checking
- Game-based local model checking for the coalgebraic \(\mu\)-calculus
- Axiomatising extended computation tree logic
- On model checking for the -calculus and its fragments
- Towards the hierarchical verification of reactive systems
- Free -lattices
- Partial-order reduction in the weak modal mu-calculus
- Model checking in the modal -calculus and generic solutions
- Compositional checking of satisfaction
- Modal and temporal logics for processes
- Games for the -calculus
- Trapping mutual exclusion in the box calculus
- Modular abstractions for verifying real-time distributed systems
- The expressive power of implicit specifications
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Compositionality and locality for improving model checking in the selective mu-calculus
- Abstract reduction in directed model checking CCS processes
- On-the-fly verification: advancements in dependency graphs (invited talk)
- Cyclic proofs in Hoare logic and its reverse
- Distributed symbolic model checking for -calculus
- Reduced models for efficient CCS verification
- \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes
- Automated analysis of mutual exclusion algorithms using CCS
- Canonical completeness of infinitary \(\mu \)
This page was built for publication: Local model checking in the modal mu-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1177939)
