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

modal mu- calculusprogram verificationtableau proof systemtransition 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

• An automata theoretic decision procedure for the propositional mu- calculus
• CTL^* and ECTL^* as fragments of the modal -calculus
• scientific article; zbMATH DE number 4119603 (Why is no real title available?)
• scientific article; zbMATH DE number 4119617 (Why is no real title available?)
• 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

(24)

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

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)