The authors present a thorough analysis of the module-checking problem, replete with detailed logic and examples. The paper is formal, and over 60 percent of it comprises theorems, lemmas, and proofs.

The focus of this paper is the intersection of formal propositional temporal logic and automata theory. The authors start by introducing the concept of model checking, which applies to verification of a closed system that does not interact with its environment. Model checking is relatively easy, they assert, in as much as the system state is independent of nondeterministic environmental influence. The behavior of a closed system is then completely determined by the state of that system. Patrice Godefroid of Bell Labs-Lucent has published a succinct relevant tutorial on Model Checking, available at http://research.microsoft.com/specncheck/docs/godefroid.pdf.

Module checking is not quite so simple. A module is, by contrast, an open system. An open system, by definition, interacts with its (external) environment. The environment influences the open system’s behavior. How then, does one verify the correctness of an open system’s behavior? It is an entirely different problem than verification of a closed system’s behavior.

The remainder of this paper is devoted to answering this question, both quantitatively and qualitatively. Much of the research interest in this area seems to reside in the EU (particularly Germany and France), and similar issues are being addressed there as in this paper. The authors close with a discussion of the differences between linear temporal logic and branching temporal logic as applied to model checking, and conclude that branching-time model checking should really be treated as branching-time MODULE checking. For those interested in further research, the authors offer nearly three pages of references.