Model checking partial state spaces with 3-valued temporal logics (extended abstract).

DOI10.1007/3-540-48683-6_25MaRDI QIDQ4818796zbMATH OpenFDO

Authors Glenn Bruns, Patrice Godefroid

Publication date 24 September 2004

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

Full work available at URL https://doi.org/10.1007/3-540-48683-6_25

Mathematics Subject Classification ID

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

Recommendations

• Implementing a multi-valued symbolic model checker
• Bounded Model Checking for Partial Kripke Structures
• From Model Checking to a Temporal Proof for Partial Models
• On the expressiveness of 3-valued models

Cited in

(47)

• An abstraction-refinement methodology for reasoning about network games
• 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
• Static analysis of topology-dependent broadcast networks
• Compositional verification and 3-valued abstractions join forces
• Model checking of linear-time properties in multi-valued systems
• Approximate verification of strategic abilities under imperfect information
• Logical vs. behavioural specifications
• A verification-driven framework for iterative design of controllers
• On finite-state approximants for probabilistic computation tree logic
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
• Modal transition systems: A foundation for three-valued program analysis
• Parameterisation of three-valued abstractions
• On the complexity of semantic self-minimization
• Using assumptions to distribute CTL model checking
• Using assumptions to distribute alternation free {\(\mu\)}-calculus model checking
• Efficient patterns for model checking partial state spaces in CTL \(\cap\) LTL
• Inherent vacuity in lattice automata
• Abstraction and abstraction refinement
• Bonsai: cutting models down to size
• Latticed Simulation Relations and Games
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Property Driven Three-Valued Model Checking on Hybrid Automata
• Don't know for multi-valued systems
• Multi-valued model checking games
• Model checking lattices: using and reasoning about information orders for abstraction
• On the expressiveness of 3-valued models
• Generalized model checking: Reasoning about partial state spaces
• Model-checking view-based partial specifications
• Integrating topological proofs with model checking to instrument iterative design
• The Complexity of Linear-Time Temporal Logic Model Repair
• Compositional specification in rewriting logic
• Lattice Automata
• Bounded Model Checking for Partial Kripke Structures
• Formal verification of three-valued digital waveforms
• Minimizing deterministic lattice automata
• Be lazy and don't care: faster CTL model checking for recursive state machines
• Information Exchange Between Over- and Underapproximating Software Analyses
• On the consistency, expressiveness, and precision of partial modeling formalisms
• Model checking branching time properties for incomplete Markov chains
• Incremental model checking for fuzzy computation tree logic
• An abstract interpretation toolkit for CRL
• On model checking multiple hybrid views
• 3-valued abstraction: More precision at less cost

This page was built for publication: Model checking partial state spaces with 3-valued temporal logics (extended abstract).

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