Efficient detection of vacuity in ACTL formulas

Abstract

Propositional logic formulas containing implications can suffer from antecedent failure, in which the formula is true trivially because the pre-condition of the implication is not satisfiable. In other words, the post-condition of the implication does not affect the truth value of the formula. We call this a vacuous pass, and extend the definition of vacuity to cover other kinds of trivial passes in temporal logic. We define w-ACTL, a subset of CTL and show by construction that for every w-ACTL formula φ there is a formula w(φ), such that: both and w(φ) are true in some model M iff φ passes vacuously. A useful side-effect of w(φ) is that if false, any counter-example is also a non-trivial witness of the original formula φ.