Temporal Antecedent Failure: Refining Vacuity

We re-examine vacuity in temporal logic model checking. We note two disturbing phenomena in recent results in this area. The first indicates that not all vacuities detected in practical applications are considered a problem by the system verifier. The second shows that vacuity detection for certain logics can be very complex and time consuming. This brings vacuity detection into an undesirable situation where the user of the model checking tool may find herself waiting a long time for results that are of no interest for her. In this paper we define Temporal Antecedent Failure, an extension of antecedent failure to temporal logic, which refines the notion of vacuity. According to our experience, this type of vacuity always indicates a problem in the model, environment or formula. On top, detection of this vacuity is extremely easy to achieve. We base our definition and algorithm on regular expressions, that have become the major temporal logic specification in practical applications.

• Type: Conference
• Year: 2007
• Where: CONCUR
• Authors: Shoham Ben-David, Dana Fisman, Sitvanit Ruah
• Keywords: CONCUR 2007, Distributed And Parallel Computing, Model Checking, Temporal Logic, Temporal Logic Model