Model Checking vs. Generalized Model Checking: Semantic Minimization for Temporal Logics

We study in this paper for which temporal-logic formulas generalized model checking can improve precision over model checking. More generally, we study how to reduce generalized model checking to model checking by a temporal-logic formula transformation, which generalizes a transformation for propositional logic known as semantic minimization in the literature. We show that many temporal-logic formulas of practical interest are self-minimizing, i.e., are their own semantic minimizations, and hence that model checking for these formulas has the same precision as generalized model checking, independently of any model.