A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness
Tom\'a\v{s} Babiak, Mojm\'ir K\v{r}et\'insk\'y, Vojt\v{e}ch, \v{R}eh\'ak, and Jan Strej\v{c}ek
TL;DR
This paper uncovers a subtle error in LTL formulas reduction used in model checking, which caused incorrect results in the DiVinE tool, and provides guidance to prevent such errors in future tools.
Contribution
It identifies a specific subtle error in LTL reduction methods and discusses its impact on model checking correctness, aiding future tool development.
Findings
The error affected the correctness of some model checking results.
The paper provides insights to avoid similar errors in future implementations.
It emphasizes the importance of rigorous validation in LTL reduction techniques.
Abstract
We identify a subtle error in LTL formulas reduction method used as one optimization step in an LTL to B\"uchi automata translation. The error led to some incorrect answers of the established model checker DiVinE. This paper should help authors of other model checkers to avoid this error.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Software Testing and Debugging Techniques