###
Verification of Open Systems

Moshe Y. Vardi

Rice University
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 verification 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.
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 describe and examine module checking problem,
and study its computational complexity. Our results show that module
checking is computationally harder than model checking.