Module checking revisited

  • Orna Kupferman
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


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.


  1. [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
  2. [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
  3. [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
  4. [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
  5. [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
  6. [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
  7. [Eme85]
    E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. LP, LNCS 193, pp. 79–87, 1985.Google Scholar
  8. [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
  9. [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
  10. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  11. [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
  12. [Jon83]
    C.B. Jones. Specification and design of (parallel) programs. In Proc. 9th IFIP, pp. 321–332, North-Holland, 1983.Google Scholar
  13. [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
  14. [KV96]
    O. Kupferman and M.Y. Vardi. Module checking. In Proc. 8th CAV, LNCS 1102, pp. 75–86, August 1996.Google Scholar
  15. [Lam83]
    L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systenms, 5:190–222, 1983.Google Scholar
  16. [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
  17. [Mil71]
    R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd IJCAI, British Computer Society, pp. 481–489, September 1971.Google Scholar
  18. [MP92]
    Z. Manna and A. Pnueli. Temporal specification and verification of reactive modules. 1992.Google Scholar
  19. [MS87]
    D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267–276, 1987.Google Scholar
  20. [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
  21. [Pnu81]
    A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.Google Scholar
  22. [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
  23. [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
  24. [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
  25. [Var95]
    M.Y. Vardi. On the complexity of modular model checking. In Proc. 10th LICS, June 1995.Google Scholar
  26. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Orna Kupferman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.EECS DepartmentUC BerkeleyBerkeleyUSA
  2. 2.Department of Computer ScienceRice UniversityHoustonUSA

Personalised recommendations