An automata-theoretic approach to modular model checking

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 interac ting. This is called the assume-guarantee paradigm. In this paper we consid er assume-guarantee specifications in which the guarantee is specified by b ranching temporal formulas. We distinguish between two approaches. In the f irst approach, the assumption is specified by branching temporal formulas t oo. In the second approach, the assumption is specified by linear temporal logic. We consider guarantees in For All CTL and For All CTL*, the universa l fragments of CTL and CTL*, and assumptions in LTL, For All CTL, and For A ll CTL*. We develop two fundamental techniques: building maximal models for For All CTL and For All CTL* formulas and using alternating; automata to o btain space-efficient algorithms for fair model checking. Using these techn iques we classify the complexity of satisfiability, validity, implication, and modular verification for For All CTL and For All CTL*. We show that mod ular verification is PSPACE-complete for For All CTL and is EXPSPACE-comple te for For All CTL*. We prove that when the assumption is linear, these bou nds hold also for guarantees in CTL and CTL*. On the other hand, the proble m remains EXPSPACE-hard even when we restrict the assumptions to LTL and ta ke the guarantee as a fixed For All CTL formula.