Enhanced vacuity detection in linear temporal logic.

DOI10.1007/B11831MaRDI QIDQ5900691zbMATH OpenOpenAlexFDO

Authors Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, A. Tiemeyer, Moshe Y. Vardi

Publication date 20 April 2010

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

Full work available at URL https://doi.org/10.1007/b11831

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1487861
• Efficient detection of vacuity in temporal model checking
• Robust vacuity for branching temporal logic
• On the Notion of Vacuous Truth
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(27)

• Before and after vacuity
• Vacuity in practice: temporal antecedent failure
• Timed vacuity
• Vacuity in synthesis
• Adaptive testing for specification coverage and refinement in CPS models
• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• Synthesizing adaptive test strategies from temporal logic specifications
• Extracting unsatisfiable cores for LTL via temporal resolution
• Robust vacuity for branching temporal logic
• Inherent vacuity in lattice automata
• Synthesizing non-vacuous systems
• Trace diagnostics using temporal implicants
• On the Notion of Vacuous Truth
• Temporal Antecedent Failure: Refining Vacuity
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• scientific article; zbMATH DE number 1487861 (Why is no real title available?)
• Linear temporal logic symbolic model checking
• scientific article; zbMATH DE number 1903373 (Why is no real title available?)
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• Sanity Checks in Formal Verification
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Efficient detection of vacuity in temporal model checking
• Coverage metrics for temporal logic model checking

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Enhanced vacuity detection in linear temporal logic.

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