Efficient Automaton Theoretical Vacuity Detection for Formal Properties

Model checking is a powerful technique for verifying the correctness of systems with respect to the requirements. While some errors happen in the property, the model itself, or the environment, we think that satisfaction of the property is meaningless (vacuous) satisfaction. It misleads users of model-checking that a system is correct. Traditional temporal logic vacuity detection is based on a syntactic definition. It is undesirable because vacuity detection would depend on syntactic formalization choices that have no effect on the semantics. This article presents an automaton-based semantic vacuity detection method which synthesizes the property into the automaton and detects the vacuity by detecting the reachability of the automaton state. Compared with the traditional syntactic-based vacuity detection, the proposed method is well suited for detecting vacuity with respect to multiple occurrences of a sub-formula. At the same time, we do not distinguish the temporal logic language. As long as the property can be synthesized into an automaton, this method can be well applied. We extend the vacuity to the satisfaction of real-time properties. The real experiments show that this method is applied efficiently in practical vacuity detection. To our knowledge, it is the first attempt to present and solve practical vacuity in an automaton view.