Generalized model checking: Reasoning about partial state spaces

DOI10.1007/3-540-44618-4_14MaRDI QIDQ4536601zbMATH OpenFDO

Authors Glenn Bruns, Patrice Godefroid

Publication date 28 November 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44618-4_14

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2102712
• Bounded Model Checking for Partial Kripke Structures
• On the complexity of semantic self-minimization
• From Model Checking to a Temporal Proof for Partial Models
• On the consistency, expressiveness, and precision of partial modeling formalisms

Cited in

(36)

• A local approach for temporal model checking of Java bytecode
• Multi-robot LTL planning under uncertainty
• TOrPEDO : witnessing model correctness with topological proofs
• Computation tree logic model checking based on multi-valued possibility measures
• Model checking of linear-time properties in multi-valued systems
• GSTE is partitioned model checking
• Three-valued temporal logic \(Q_t\) and future contingents
• A semantic framework for the abstract model checking of tccp programs
• On finite-state approximants for probabilistic computation tree logic
• On the complexity of semantic self-minimization
• Efficient patterns for model checking partial state spaces in CTL \(\cap\) LTL
• Abstraction and abstraction refinement
• Model checking of reachability problems based on generalized possibility measures
• Model Checking Value-Passing Modal Specifications
• LTL Generalized Model Checking Revisited
• Mixed Transition Systems Revisited
• Symbolic Model Checking of Tense Logics on Rational Kripke Models
• Modal transition systems with weight intervals
• Model-checking view-based partial specifications
• Falsifying safety properties through games on over-approximating models
• Integrating topological proofs with model checking to instrument iterative design
• Compositional specification in rewriting logic
• EXPTIME-complete decision problems for modal and mixed specifications
• More Precise Partition Abstractions
• Better Under-Approximation of Programs by Hiding Variables
• Model Checking for Action Abstraction
• Complexity of Decision Problems for Mixed and Modal Specifications
• Bounded Model Checking for Partial Kripke Structures
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• On the consistency, expressiveness, and precision of partial modeling formalisms
• Incremental model checking for fuzzy computation tree logic
• The modal logic of abstraction refinement
• Data structures for symbolic multi-valued model-checking
• On model checking multiple hybrid views
• Comparing disjunctive modal transition systems with an one-selecting variant
• 3-valued abstraction: More precision at less cost

This page was built for publication: Generalized model checking: Reasoning about partial state spaces

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