Local model checking for infinite state spaces

DOI10.1016/0304-3975(92)90183-GMaRDI QIDQ1190489zbMATH OpenOpenAlexFDO

Authors Julian Bradfield, Colin Stirling

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

zbMATH Keywords

program verificationtransition systemmodal mu- calculustableau proof system

Mathematics Subject Classification ID

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)

Recommendations

• scientific article; zbMATH DE number 1499079
• Tableau-based model checking in the propositional mu-calculus
• Local model checking in the modal mu-calculus
• Compositionality and locality for improving model checking in the selective mu-calculus
• Automated Technology for Verification and Analysis

Cites work

• scientific article; zbMATH DE number 4119603 (Why is no real title available?)
• scientific article; zbMATH DE number 4119617 (Why is no real title available?)
• An automata theoretic decision procedure for the propositional mu- calculus
• CTL^* and ECTL^* as fragments of the modal -calculus
• Local model checking in the modal mu-calculus
• Modal logics for communicating systems
• Proof methods for modal and intuitionistic logics
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Results on the propositional \(\mu\)-calculus
• SnS can be modally characterized

Cited in

(20)

• Proving properties of dynamic process networks
• Modular abstractions for verifying real-time distributed systems
• Automated temporal reasoning about reactive systems
• Modal and temporal logics for processes
• Liveness checking as safety checking for infinite state spaces
• Computer says no: verdict explainability for runtime monitors using a local proof system
• Compositionality and locality for improving model checking in the selective mu-calculus
• Symbolic bisimulations
• Tableau-based model checking in the propositional mu-calculus
• CTL^* and ECTL^* as fragments of the modal -calculus
• Towards the hierarchical verification of reactive systems
• State Space Representation for Verification of Open Systems
• A local approach for temporal model checking of Java bytecode
• Selective mu-calculus and formula-based equivalence of transition systems
• Ensuring completeness of symbolic verification methods for infinite-state systems
• On global induction mechanisms in aμ-calculus with explicit approximations
• Property-oriented expansion
• scientific article; zbMATH DE number 1790379 (Why is no real title available?)
• Model checking properties on reduced trace systems
• Bounded model checking of infinite state systems

This page was built for publication: Local model checking for infinite state spaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1190489)