Abstract
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 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-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is 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 is 2EXPTIME-cornplete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Aziz, T.R. Shiple, V. Singhal, and A.L. Sangiovanni-Vincentelli. Formula-dependent equivalence for compositional CTL model checking. In Proc. 6th Conf. on Computer Aided Verification, Volume 818 of Lecture Notes in Computer Science, pages 324–337, Stanford, CA, June 1994. Springer-Verlag.
I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Workshop on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 182–193, Stanford, June 1994.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428–439, Philadelphia, June 1990.
O. Bernholtz and O. Grumberg. Buy one, get one free !!! In Proceedings of the First International Conference on Temporal Logic, Volume 827 of Lecture Notes in Artificial Intelligence, pages 210–224, Bonn, July 1994. Springer-Vertag.
M.C. Browne. An improved algorithm for the automatic verification of finite state systems using temporal logic. In Proceedings of the First Symposium on Logic in Computer Science, pages 260–266, Cambridge, June 1986.
O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D. L. Dill, editor, Computer Aided Verification, Proc. 6th Int. Conference, Volume 818 of Lecture Notes in Computer Science, pages 142–155, Stanford, June 1994. Springer-Verlag, Berlin.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.
E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Decade of Concurrency — Reflections and Perspectives (Proceedings of REX School), Lecture Notes in Computer Science, pages 124–175. Springer-Verlag, 1993.
R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in System Design, 2:121–147, 1993.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151–178, 1986.
E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.
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.
E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pages 997–1072, 1990.
E.A. Emerson and A.P. Sistla. Deciding branching time logic. In Proceedings of the 16th ACM Symposium on Theory of Computing, Washington, April 1984.
M.J. Fischer and R.E. Ladner. Prepositional dynamic logic of regular programs. J. of Computer and Systems Sciences, 18:194–211, 1979.
R.W. Floyd. Assigning meaning to programs. In Proceedings Symposium on Applied Mathematics, volume 19, 1967.
M.J. Fischer and L.D. Zuck. Reasoning about uncertainty in fault-tolerant distributed systems. In M. Joseph, editor, Proc. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 142–158. Springer-Verlag, 1988.
M. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-completeness. W. Freeman and Co., San Francisco, 1979.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3): 843–871, 1994.
L.M. Goldschlager. The monotone and planar circuit value problems are log space complete for p. SIGACT News, 9(2):25–29, 1977.
C.A.R. Hoare. An axiomatic basis of computer programming. Communications of the ACM, 12(10):576–583, 1969.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
D. Harel and A. Pnueli. On the development of reactive systems. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477–498. Springer-Verlag, 1985.
O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In Computer Aided Verification, Proc. 7th Int. Workshop, pages 325–338, Liege, July 1995.
O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, pages 408–422, Philadelphia, August 1995.
L. Lamport. Sometimes is sometimes “not never” — on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174–185, January 1980.
K.G. Larsen. Modal specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 232–246, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
D.E. Long. Model checking, abstraction and compositional verification. PhD thesis, Carnegie-Mellon University, Pittsburgh, 1993.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97–107, New Orleans, January 1985.
K.G. Larsen and G.B. Thomsen. A modal process logic. In Proceedings of the 3th Symposium on Logic in Computer Science, Edinburgh, 1988.
K.L. McMillan. Symbolic model checking. Kluwer Academic Publishers, 1993.
Z. Manna and A. Pnueli. Temporal specification and verification of reactive modules. 1992.
A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57,1977.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, Austin, Januery 1989.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int'l Symp. on Programming, volume 137, pages 337–331. Springer-Verlag, Lecture Notes in Computer Science, 1981.
M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1–35, 1969.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. J. ACM, 32:733–749, 1985.
M.Y. Vardi. On the complexity of modular model checking. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science, June 1995.
M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240–251, 1985.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Vardi, M.Y. (1996). Module checking. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_59
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_59
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive