Branching-Time Temporal Logics with Minimal Model Quantifiers

Temporal logics are a well investigated formalism for the specification and verification of reactive systems. Using formal verification techniques, we can ensure the correctness of a system with respect to its desired behavior (specification), by verifying whether a model of the system satisfies a temporal logic formula modeling the specification. From a practical point of view, a very challenging issue in using temporal logic in formal verification is to come out with techniques that automatically allow to select small critical parts of the system to be successively verified. Another challenging issue is to extend the expressiveness of classical temporal logics, in order to model more complex specifications. In this paper, we address both issues by extending the classical branching-time temporal logic Ctl* with minimal model quantifiers (MCtl*). These quantifiers allow to extract, from a model, minimal submodels on which we check the specification (also given by an MCtl* formula).We show that MCtl* is strictly more expressive than Ctl*. Nevertheless, we prove that the model checking problem for MCtl. remains decidable and in particular in PSpace. Moreover, differently from Ctl*, we show that MCtl* does not have the tree model property, is not bisimulation-invariant and is sensible to unwinding. As far as the satisfiability concerns, we prove that MCtl* is highly undecidable. We further investigate the model checking and satisfiability problems for MCtl* sublogics, such as MPml, MCtl, and MCtl+, for which we obtain interesting results. Among the others, we show that MPml retains the finite model property and the decidability of the satisfiability problem.