Portal de Periódicos da CAPES

Modular Model Checking

1998; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-49213-5_14

1611-3349

Orna Kupferman, Moshe Y. Vardi,

Safety Systems Engineering in Autonomy

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the assume-guarantee paradigm. In this paper we consider assume-guarantee specifications in which the guarantee is specified by branching temporal formulas. We distinguish between two approaches. In the first approach, the assumption is specified by branching temporal formulas. In the second approach, the assumption is specified by linear temporal logic. We consider guarantees in ∀CTL and ∀CTL; the universal fragments of CTL and CTL, and assumptions in LTL, ∀CTL, and ∀CTL. We describe a reduction of modular model checking to standard model checking. Using the reduction, we show that modular model checking is PSPACE-complete for ∀CTL and is EXPSPACE-complete for ∀CTL. We then show that the case of LTL assumption is a special case of the case of ∀CTL assumption, but that the EXPSPACE-hardness result apply already to assumptions in LTL.