Branching-Time Temporal Logics with Minimal Model Quantifiers

Abstract. 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 formul...

• Type: Journal
• Year: 2009
• Where: DLT
• Authors: Fabio Mogavero, Aniello Murano
• Keywords: DLT 2009, Model, Specification, Temporal Logic, Theoretical Computer Science