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 env
ironment and whose behavior depends on this interaction. The ability of tem
poral logics to describe an ongoing interaction of a reactive program with
its environment makes them particularly appropriate for the specification o
f open systems. Nevertheless, model-checking algorithms used for the verifi
cation of closed systems are not appropriate for the verification of open s
ystems. 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-checkin
g algorithms and tools.
In this paper we introduce and examine the problem of model checking of ope
n systems (module checking, for short). We show that while module checking
and model checking coincide for the linear-time paradigm, module checking i
s 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 2EXPTIME-complete for specifications in CTL*. This bad news is
also carried over when we consider the program-complexity of module checkin
g. As good news, we show that for the commonly-used fragment of CTL (univer
sal, possibly, and always possibly properties), current model-checking tool
s do work correctly, or can be easily adjusted to work correctly, with resp
ect to both closed and open systems. (C) 2001 Academic Press.