Semantic Vacuity

The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the syntax of a temporal logic. They are therefore syntactic: whether a model vacuously satisfies a formula is affected by semantics-preserving changes to the formula. This leads to inconsistent and counter-intuitive results. We propose an alternative: a semantic definition of vacuity for LTL where either two semantically equivalent LTL formulas are both satisfied vacuously in a model, or neither of them are. Our definition is based on a syntactic-invariant separation of LTL formulas, which gives rise to an algorithm for detecting semantic vacuity using trap properties. We also propose an alternative algorithm for Buchi automata, which can be used to detect the vacuous satisfaction of omega-regular properties as well as LTL formulas. We analyze this algorithm´s worst-case complexity and, using real-world examples, demonstrate that semantic vacuity can be efficiently decided in practice.