Local model checking in the modal mu-calculus
From MaRDI portal
Publication:1177939
DOI10.1016/0304-3975(90)90110-4zbMath0745.03027OpenAlexW1992582873MaRDI 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 logictemporal logicconcurrencytransition systemstableau methodCCSmodal mu-calculusanalysis of Knuth's mutual exclusion algorithmsatisfiability in finite models
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS, Bounded model checking of infinite state systems, Two Ways to Common Knowledge, \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes, Discrete tense logic with infinitary inference rules and systematic frame constants: A Hilbert-style axiomatization, Towards the hierarchical verification of reactive systems, Proving properties of dynamic process networks, Axiomatising extended computation tree logic, Petri nets, traces, and local model checking, Partial-order reduction in the weak modal mu-calculus, Multi-valued model checking games, Unnamed Item, Automated analysis of mutual exclusion algorithms using CCS, Local Model Checking in a Logic for True Concurrency, A graphical \(\mu\)-calculus and local model checking., Canonical completeness of infinitary \(\mu \), Games for the \(\mu\)-calculus, Axiomatising extended computation tree logic, Trapping mutual exclusion in the box calculus, Local model checking for infinite state spaces, Symbolic model checking: \(10^{20}\) states and beyond, Tableaux and algorithms for Propositional Dynamic Logic with Converse, Modular abstractions for verifying real-time distributed systems, The expressive power of implicit specifications, Computer says no: verdict explainability for runtime monitors using a local proof system, The Recursion Scheme from the Cofree Recursive Comonad, Formal Verification of Concurrent Systems via Directed Model Checking, On model checking for the \(\mu\)-calculus and its fragments, A local approach for temporal model checking of Java bytecode, Abstract reduction in directed model checking CCS processes, On complexity of verification of interacting agents' behavior, Quantification over sets of possible worlds in branching-time semantics, A Note on Negative Tagging for Least Fixed-Point Formulae, Free \(\mu\)-lattices, On global induction mechanisms in aμ-calculus with explicit approximations, Polynomial-Time Under-Approximation of Winning Regions in Parity Games, Petri nets, traces, and local model checking, A compositional \(\mu\)-calculus proof system for statecharts processes, Model checking for hybrid logic, Using heuristic search for finding deadlocks in concurrent systems, 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 \(\mu\)-calculus in the calculus of inductive constructions, Distributed symbolic model checking for \(\mu\)-calculus, Reduced models for efficient CCS verification
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
