Modular model checking

Abstract

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 VCTL and VCTL*, the universal fragments of CTL and CTL*, and assumptions in LTL, VCTL, and VCTL*. 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 VCTL and is EXPSPACE-complete for VCTL*. We then show that the case of LTL assumption is a special case of the case of VCTL* assumption, but that the EXPSPACE-hardness result apply already to assumptions in LTL.