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. 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 describe a reduction of
modular model checking to standard model checking. Using the reduction,
we show that modular model checking is PSPACE-complete for ACTL and is
EXPSPACE-complete for ACTL*. We then show that the case of LTL
assumption is a special case of the case of ACTL* assumption, but that
the EXPSPACE-hardness result apply already to assumptions in LTL.