On the Complexity of 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 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 too. In the
second approach, the assumption is specified by linear temporal logic.

We consider guarantees in ACTL and ACTL*, the universal fragments of
CTL and CTL*, and assumptions in LTL, ACTL, and ACTL*. We develop two
fundamental techniques: building maximal models for ACTL and ACTL*
formulas and using alternating automata to obtain space-efficient
algorithms for fair model checking. Using these techniques we classify
the complexity of satisfiability, validity, implication, and modular
verification for ACTL and ACTL*. We show that modular verification is
PSPACE-complete for ACTL and is is EXPSPACE-complete for ACTL. We
prove that when the assumption is linear, these bounds hold also for
guarantees in CTL and CTL*. On the other hand,the problem remains
EXPSPACE-hard even when we restrict the assumptions to LTL and take
the guarantee as a fixed ACTL formula.