Local model checking in the modal mu-calculus
From MaRDI portal
Publication:1177939
DOI10.1016/0304-3975(90)90110-4zbMath0745.03027MaRDI QIDQ1177939
Publication date: 26 June 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(90)90110-4
dynamic logic; temporal logic; concurrency; transition systems; tableau method; CCS; modal mu-calculus; analysis of Knuth's mutual exclusion algorithm; satisfiability in finite models
03B45: Modal logic (including the logic of norms)
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
A Note on Negative Tagging for Least Fixed-Point Formulae, Games for the \(\mu\)-calculus, Trapping mutual exclusion in the box calculus, Modular abstractions for verifying real-time distributed systems, The expressive power of implicit specifications, Local model checking for infinite state spaces, Symbolic model checking: \(10^{20}\) states and beyond, A compositional \(\mu\)-calculus proof system for statecharts processes, CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Proving properties of dynamic process networks, Axiomatising extended computation tree logic, Petri nets, traces, and local model checking, Discrete tense logic with infinitary inference rules and systematic frame constants: A Hilbert-style axiomatization
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Modal logics for communicating systems
- Results on the propositional \(\mu\)-calculus
- A refinement calculus for specifications in Hennessy-Milner logic with recursion
- Automated analysis of mutual exclusion algorithms using CCS
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- Tableau-based model checking in the propositional mu-calculus
- A modal characterization of observational congruence on finite terms of CCS
- Algebraic laws for nondeterminism and concurrency
