Efficient detection of vacuity in temporal model checking

DOI10.1023/A:1008779610539zbMath0988.68111OpenAlexW1497843565MaRDI QIDQ5943261

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

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

temporal logicmodel checking toolsvacuity

Mathematics Subject Classification ID

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

Related Items

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Analysing sanity of requirements for avionics systems ⋮ Symbolic Trajectory Evaluation ⋮ Coverage metrics for temporal logic model checking ⋮ Data structures for symbolic multi-valued model-checking ⋮ Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis ⋮ Inherent Vacuity in Lattice Automata ⋮ On the Notion of Vacuous Truth ⋮ Synthesizing Non-Vacuous Systems ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Linear temporal logic symbolic model checking ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Beyond vacuity: towards the strongest passing formula ⋮ Vacuity in practice: temporal antecedent failure ⋮ Timed vacuity ⋮ Synthesizing adaptive test strategies from temporal logic specifications ⋮ Vacuity in synthesis ⋮ Before and after vacuity