Module Checking Revisited
-------------------------

When we verify the correctness of an open system with respect to a
desired requirement, we should take into consideration the different
environments with which the system may interact. Each environment
induces a different behavior of the system, and we want all these
behaviors to satisfy the requirement. Module checking is an
algorithmic method that checks, given an open system (modeled as a
finite structure) and a desired requirement (specified by a
temporal-logic formula), whether the open system satisfies the
requirement with respect to all environments. In this paper we extend
the module-checking method with respect to two orthogonal issues. Both
issues concern the fact that often we are not interested in
satisfaction of the requirement with respect to all environments, but
only with respect to these that meet some restriction. We consider the
case where the environment has incomplete information about the
system; i.e., when the system has internal variables, which are not
readable by its environment, and the case where some assumptions are
known about environment; i.e., when the system is guaranteed to
satisfy the requirement only when its environment satisfies certain
assumptions. We study the complexities of the extended module-checking
problems. In particular, we show that for universal temporal logics
(e.g., LTL, ACTL, and ACTL*), module checking with incomplete
information coincides with module checking, which by itself coincides
with model checking. On the other hand, for non-universal temporal
logics (e.g., CTL and CTL*), module checking with incomplete
information is harder than module checking, which is by itself harder
than model checking.