Local model checking for infinite state spaces
From MaRDI portal
Publication:1190489
DOI10.1016/0304-3975(92)90183-GzbMath0747.68036OpenAlexW2097026217MaRDI QIDQ1190489
Colin Stirling, Julian Bradfield
Publication date: 26 September 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(92)90183-g
Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (13)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Bounded model checking of infinite state systems ⋮ Towards the hierarchical verification of reactive systems ⋮ Proving properties of dynamic process networks ⋮ Selective mu-calculus and formula-based equivalence of transition systems ⋮ Model checking properties on reduced trace systems ⋮ Symbolic bisimulations ⋮ Modular abstractions for verifying real-time distributed systems ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ A local approach for temporal model checking of Java bytecode ⋮ On global induction mechanisms in aμ-calculus with explicit approximations ⋮ Property-oriented expansion
Cites Work
- Unnamed Item
- Unnamed Item
- Modal logics for communicating systems
- Results on the propositional \(\mu\)-calculus
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- SnS can be modally characterized
- Proof methods for modal and intuitionistic logics
- An automata theoretic decision procedure for the propositional mu- calculus
- Local model checking in the modal mu-calculus
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
This page was built for publication: Local model checking for infinite state spaces
