Module Checking
---------------

In computer system design, we distinguish between closed and
open systems. A closed system is a system whose behavior is
completely determined by the state of the system. 
An open system is a system that interacts with its environment and
whose behavior depends on this interaction.  
The ability of temporal logics to describe an ongoing interaction of a
reactive program with its environment makes them particularly
appropriate for the specification of open systems. 
Nevertheless, model-checking algorithms used for the verification of
closed systems are not appropriate for the verification of open
systems. Correct model checking of open systems should check the
system with respect to arbitrary environments and should take into 
account uncertainty regarding the environment. This is not the case
with current model-checking algorithms and tools.

In this paper we introduce and examine the problem of 
model checking of open systems (module checking, for short).
We show that while module checking and model checking coincide
for the linear-time paradigm, module checking is much harder 
than model checking for the branching-time paradigm.
We prove that the problem of module checking is EXPTIME-complete for
specifications in CTL and is 2EXPTIME-complete for specifications in
CTL*. This bad news is also carried over when we consider
the program-complexity of module checking. As good news, we show that
for the commonly-used fragment of CTL (universal, possibly, and always
possibly properties), current model-checking tools do work correctly,
or can be easily adjusted to work correctly,  with respect to both
closed and open systems.