# Module checking revisited

## Abstract

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, ∀CTL, and ∀CTL*), 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.

## References

- [BVW94]O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In
*Proc. 6th CAV*, LNCS 818, pp. 142–155, June 1994.Google Scholar - [CE81]E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In
*Proc. LP*, LNCS 131, pp. 52–71, 1981.Google Scholar - [CGB86]E.M. Clarke, O. Grumberg, and M.C. Browne. Reasoning about networks with many identical finite-state processes. In
*Proc. 5th PODC*, pp. 240–248, August 1986.Google Scholar - [CES86]E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications.
*ACM TPLS*, 8(2):244–263, 1986.Google Scholar - [EJ88]E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In
*Proc. 29th FOCS*, pp. 368–377, October 1988.Google Scholar - [EL85]E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In
*Proc. 18th Hawaii International Conference on System Sciences*, Hawaii, 1985.Google Scholar - [Eme85]E.A. Emerson. Automata, tableaux, and temporal logics. In
*Proc. LP*, LNCS 193, pp. 79–87, 1985.Google Scholar - [FZ88]M.J. Fischer and L.D. Zuck. Reasoning about uncertainty in fault-tolerant distributed systems. In
*Proc. Formal Techniques in Real-Time and Fault-Tolerant Sys.*, LNCS 331, pp. 142–158, 1988.Google Scholar - [GL94]O. Grumberg and D.E. Long. Model checking and modular verification.
*ACM Trans. on Programming Languages and Systems*, 16(3):843–871, 1994.Google Scholar - [Hoa85]C.A.R. Hoare.
*Communicating Sequential Processes*. Prentice-Hall, 1985.Google Scholar - [HP85]D. Harel and A. Pnueli. On the development of reactive systems. In
*Logics and Models of Concurrent Systems*, volume F-13 of*NATO Advanced Summer Institutes*, pp. 477–498, 1985.Google Scholar - [Jon83]C.B. Jones. Specification and design of (parallel) programs. In
*Proc. 9th IFIP*, pp. 321–332, North-Holland, 1983.Google Scholar - [KV95]O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In
*Proc. 6th CONCUR*, LNCS 962, pp. 408–422, August 1995.Google Scholar - [KV96]O. Kupferman and M.Y. Vardi. Module checking. In
*Proc. 8th CAV*, LNCS 1102, pp. 75–86, August 1996.Google Scholar - [Lam83]L. Lamport. Specifying concurrent program modules.
*ACM Trans. on Programming Languages and Systenms*, 5:190–222, 1983.Google Scholar - [LP85]O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In
*Proc. 12th POPL*, pp. 97–107, January 1985.Google Scholar - [Mil71]R. Milner. An algebraic definition of simulation between programs. In
*Proc. 2nd IJCAI*, British Computer Society, pp. 481–489, September 1971.Google Scholar - [MP92]Z. Manna and A. Pnueli. Temporal specification and verification of reactive modules. 1992.Google Scholar
- [MS87]D.E. Muller and P.E. Schupp. Alternating automata on infinite trees.
*Theoretical Computer Science*, 54,:267–276, 1987.Google Scholar - [MS95]D.E. Muller and P.E. Schupp. Simulating aternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra.
*Theoretical Computer Science*, 141:69–107, 1995.Google Scholar - [Pnu81]A. Pnueli. The temporal semantics of concurrent programs.
*Theoretical Computer Science*, 13:45–60, 1981.Google Scholar - [Pnu85]A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In
*Proc. Advanced School on Current Trends in Concurrency*, LNCS 224, pp. 510–584, 1985.Google Scholar - [QS81]J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In
*Proc. 5th International Symp. on Programming*, LNCS 137, pp. 337–351, 1981.Google Scholar - [Rei84]J.H. Reif. The complexity of two-player games of incomplete information.
*J. on Computer and System Sciences*, 29:274–301, 1984.Google Scholar - [Var95]M.Y. Vardi. On the complexity of modular model checking. In
*Proc. 10th LICS*, June 1995.Google Scholar - [VW86]M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs.
*Journal of Computer and System Science*, 32(2): 182–221, April 1986.Google Scholar