Minimal Model Quantifiers

Abstract

Temporal logics are a well investigated formalism for the specification and verification of reactive systems. Using formal verification techniques, one can ensure the correctness of a system with respect to a desired behavior, i.e., the specification, by verifying whether a model of the former satisfies a temporal logic formula expressing the latter. In this setting, a very crucial aspect is to reasoning about substructures of the entire model. Indeed, for several fundamental problems, the formal verification approach requires to select a portion of the model of interest on which to verify a specific property. In this paper, we introduce a new logic framework that allows to select automatically desired parts of the system to be successively verified. Specifically, we extend the classical branching-time temporal logic Ctl $^{*}$ by means of minimal model operators (MCtl $^{*}$, for short). These operators allow to extract, from a model, minimal submodels on which we can check a specification, which is also given by an MCtl $^{*}$ formula. We interpret the logic under three different semantics, called minimal ($m$), minimal-unwinding ($mu$), and unwinding-minimal ($um$), which differ one from another on the way a substructure is extracted and then checked in the verification process. We show that both MCtl $^{*}$ $_{m}$ and MCtl $^{*}$ $_{mu}$ are strictly more expressive than Ctl $^{*}$, since these logics are sensible to unwinding and not invariant under bisimulation. Conversely, MCtl $^{*}$ $_{um}$ preserves both these properties. As far as the satisfiability concerns, we prove that MCtl $^{*}$ $_{m}$ and MCtl $^{*}$ $_{mu}$ are highly undecidable. We further investigate some syntactic fragments of MCtl $^{*}$, such as MCtl, for which we obtain interesting results.