zbMATH — the first resource for mathematics

Module checking. (English) Zbl 1003.68071
Summary: 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 2EXPTIME-complete 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.

MSC:
 68Q60 Specification and verification (program logics, model checking, etc.) 03B44 Temporal logic 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
CESAR
Full Text:
References:
 [1] Alur, R.; Henzinger, T.A.; Kupferman, O., Alternating-time temporal logic, Proc. 38th IEEE symposium on foundations of computer science, florida, (1997) [2] Abadi, M.; Lamport, L.; Wolper, P., Realizable and unrealizable concurrent program specifications, Proc. 16th int. colloquium on automata, languages and programming, Lecture notes in computer science, 372, (1989), Springer-Verlag Berlin/New York, p. 1-17 [3] Antoniotti, M., Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the control-D system, (1995), New York University New York [4] Aziz, A.; Shiple, T.R.; Singhal, V.; Sangiovanni-Vincentelli, A.L., Formula-dependent equivalence for compositional CTL model checking, Proc. 6th conf. on computer aided verification, Stanford, CA, Lecture notes in computer science, 818, (1994), Springer-Verlag Berlin/New York, p. 324-337 [5] Beer, I.; Ben-David, S.; Geist, D.; Gewirtzman, R.; Yoeli, M., Methodology and system for practical formal verification of reactive hardware, Proc. 6th conference on computer aided verification, Stanford, CA, Lecture notes in computer science, 818, (1994), p. 182-193 [6] Browne, M.C.; Clarke, E.M.; Grumberg, O., Characterizing finite Kripke structures in propositional temporal logic, Theoret. comput. sci., 59, 115-131, (1988) · Zbl 0677.03011 [7] Burch, J.R.; Clarke, E.M.; McMillan, K.L.; Dill, D.L.; Hwang, L.J., Symbolic model checking: 10^{20} states and beyond, Proc. 5th symposium on logic in computer science, Philadelphia, (1990), p. 428-439 [8] Clarke, E.M.; Emerson, E.A., Design and synthesis of synchronization skeletons using branching time temporal logic, Proc. workshop on logic of programs, Lecture notes in computer science, 131, (1981), Springer-Verlag Berlin/New York, p. 52-71 [9] Clarke, E.M.; Emerson, E.A.; Sistla, A.P., Automatic verification of finite-state concurrent system using temporal logic specifications, ACM trans. programming lang. systems, 8, 244-263, (1986) · Zbl 0591.68027 [10] Clarke, E.M.; Grumberg, O.; Long, D., Verification tools for finite-state concurrent systems, (), 124-175 [11] Cleaveland, R., A linear-time model-checking algorithm for the alternation-free modal μ-calculus, Formal methods in system design, 2, 121-147, (1993) · Zbl 0772.68038 [12] Emerson, E.A.; Halpern, J.Y., Sometimes and not never revisited: on branching versus linear time, J. assoc. comput. Mach., 33, 151-178, (1986) · Zbl 0629.68020 [13] Emerson, E.A.; Jutla, C., The complexity of tree automata and logics of programs, Proc. 29th IEEE symposium on foundations of computer science, white plains, (1988), p. 368-377 [14] Emerson, E.A.; Lei, C.-L., Temporal model checking under generalized fairness constraints, Proc. 18th hawaii international conference on system sciences, north hollywood, (1985), Western Periodicals [15] Emerson, E.A., Temporal and modal logic, Handbook of theoretical computer science, (1990), p. 997-1072 · Zbl 0900.03030 [16] Emerson, E.A.; Sistla, A.P., Deciding branching time logic, Proc. 16th ACM symposium on theory of computing, Washington, (1984) · Zbl 0593.03007 [17] Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, J. comput. systems sci., 18, 194-211, (1979) · Zbl 0408.03014 [18] Floyd, R.W., Assigning meaning to programs, Proceedings symposium on applied mathematics, (1967) · Zbl 0189.50204 [19] Fischer, M.J.; Zuck, L.D., Reasoning about uncertainty in fault-tolerant distributed systems, (), 142-158 [20] Garey, M.; Johnson, D.S., Computers and intractability: A guide to the theory of NP-completeness, (1979), Freeman San Francisco · Zbl 0411.68039 [21] Grumberg, O.; Long, D.E., Model checking and modular verification, ACM trans. programming languages systems, 16, 843-871, (1994) [22] Goldschlager, L.M., The monotone and planar circuit value problems are log space complete for P, SIGACT news, 9, 25-29, (1977) [23] Hoare, C.A.R., An axiomatic basis of computer programming, Commun. assoc. comput. Mach., 12, 576-583, (1969) · Zbl 0179.23105 [24] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs · Zbl 0637.68007 [25] Harel, D.; Pnueli, A., On the development of reactive systems, (), 477-498 · Zbl 0581.68046 [26] Kupferman, O.; Grumberg, O., Buy one, get one free!!!, Logic comput., 6, 523-539, (1996) · Zbl 0857.03009 [27] Kozen, D., Results on the propositional μ-calculus, Theoret. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007 [28] Kupferman, O., Augmenting branching temporal logics with existential quantification over atomic propositions, J. logic comput., 7, 1-14, (1997) [29] Kupferman, O.; Vardi, M.Y., On the complexity of branching modular model checking, Proc. 6th conference on concurrency theory, Philadelphia, Lecture notes in computer science, 962, (1995), Springer-Verlag Berlin/New York, p. 408-422 [30] Kupferman, O.; Vardi, M.Y.; Wolper, P., An automata-theoretic approach to branching-time model checking, Assoc. comput. Mach., 42, (2000) · Zbl 1133.68376 [31] Lamport, L., Sometimes is sometimes “not never”—on the temporal logic of programs, Proc. 7th ACM symposium on principles of programming languages, (1980), p. 174-185 [32] Larsen, K.G., Modal specifications, Automatic verification methods for finite state systems, proc. int. workshop, Grenoble, Lecture notes in computer science, 407, (1989), Springer-Verlag Berlin/New York, p. 232-246 [33] Long, D.E., Model checking, abstraction and compositional verification, (1993), Carnegie-Mellon University Pittsburgh [34] Lichtenstein, O.; Pnueli, A., Checking that finite state concurrent programs satisfy their linear specification, Proc. 12th ACM symposium on principles of programming languages, new orleans, (1985), p. 97-107 [35] Larsen, K.G.; Thomsen, G.B., A modal process logic, Proc. 3th symposium on logic in computer science, Edinburgh, (1988) [36] McMillan, K.L., Symbolic model checking, (1993), Kluwer Academic Dordrecht/Norwell · Zbl 1132.68474 [37] Milner, R., An algebraic definition of simulation between programs, Proc. 2nd international joint conference on artificial intelligence, (1971), British Computer Society, p. 481-489 [38] Manna, Z, and, Pnueli, A. 1992, Temporal specification and verification of reactive modules. · Zbl 0753.68003 [39] Pnueli, A., The temporal logic of programs, Proc. 18th IEEE symposium on foundation of computer science, (1977), p. 46-57 [40] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, Proc. 16th ACM symposium on principles of programming languages, Austin, (1989) · Zbl 0686.68015 [41] Pnueli, A.; Rosner, R., On the synthesis of an asynchronous reactive module, Proc. 16th int. colloquium on automata, languages and programming, Lecture notes in computer science, 372, (1989), Berlin/New YorkSpringer-Verlag, p. 652-671 [42] Pratt, V.R., A near-optimal method for reasoning about action, J. comput. system sci., 20, 231-254, (1980) · Zbl 0424.03010 [43] Queille, J.P.; Sifakis, J., Specification and verification of concurrent systems in cesar, Proc. 5th international symp. on programming, Lecture notes in computer science, 127, (1981), Springer-Verlag Berlin/New York, p. 337-351 · Zbl 0482.68028 [44] Rabin, M.O., Decidability of second order theories and automata on infinite trees, Trans. amer. math. soc., 141, 1-35, (1969) · Zbl 0221.02031 [45] Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logic, J. assoc. comput. Mach., 32, 733-749, (1985) · Zbl 0632.68034 [46] Vardi, M.Y., On the complexity of modular model checking, Proc. 10th IEEE symposium on logic in computer science, (1995) [47] Vardi, M.Y.; Stockmeyer, L., Improved upper and lower bounds for modal logics of programs, Proc 17th ACM symp. on theory of computing, (1985), p. 240-251 [48] Vardi, M.Y.; Wolper, P., An automata-theoretic approach to automatic program verification, Proc. first symposium on logic in computer science, (1986), p. 322-331 [49] Vardi, M.Y.; Wolper, P., Automata-theoretic techniques for modal logics of programs, J. comput. system sci., 32, 182-221, (1986) · Zbl 0622.03017 [50] Vardi, M.Y.; Wolper, P., Reasoning about infinite computations, Inform. and comput., 115, 1-37, (1994) · Zbl 0827.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.