Efficient detection of vacuity in temporal model checking

DOI10.1023/A:1008779610539MaRDI QIDQ5943261zbMATH OpenOpenAlexFDO

Authors Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh

Publication date 9 April 2002

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1008779610539

zbMATH Keywords

model checking toolstemporal logicvacuity

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1487861
• Before and after vacuity
• Enhanced vacuity detection in linear temporal logic.
• scientific article; zbMATH DE number 1903373
• Formal Methods in Computer-Aided Design

Cited in

(26)

• Before and after vacuity
• Vacuity in practice: temporal antecedent failure
• Timed vacuity
• Vacuity in synthesis
• Beyond vacuity: towards the strongest passing formula
• Synthesizing adaptive test strategies from temporal logic specifications
• Generation of minimum tree-like witnesses for existential CTL
• Extracting unsatisfiable cores for LTL via temporal resolution
• Analysing sanity of requirements for avionics systems
• Inherent vacuity in lattice automata
• Synthesizing non-vacuous systems
• Vacuity checking in the modal mu-calculus
• Symbolic trajectory evaluation
• On the Notion of Vacuous Truth
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• scientific article; zbMATH DE number 1487861 (Why is no real title available?)
• Finding boundary elements in ordered sets with application to safety and requirements analysis
• Linear temporal logic symbolic model checking
• An Experimental Spatio-Temporal Model Checker
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Enhanced vacuity detection in linear temporal logic.
• Monotonicity characterizations of regular languages
• Monotonicity characterizations of regular languages
• Coverage metrics for temporal logic model checking
• Data structures for symbolic multi-valued model-checking

This page was built for publication: Efficient detection of vacuity in temporal model checking

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