Steven M. German
Abstract
Methods are given for automatically verifying temporal properties of concurrent systems containing an arbitrary number of finite-state processes that communicate using CCS actions. TWo models of systems are considered. Systems in the first model consist of a unique control process and an arbitrary number of user processes with identical definitions. For this model, a decision procedure to check whether all the executions of a process satisfy a given specification is presented. This algorithm runs in time double exponential in the sizes of the control and the user process definitions. It is also proven that it is decidable whether all the fair executions of a process satisfy a given specification. The second model is a special case of the first. In this model, all the processes have identical definitions. For this model, an efficient decision procedure is presented that checks if every execution of a process satisfies a given temporal logic specification. This algorithm runs in time polynomial in the size of the process definition. It is shown how to verify certain global properties such as mutual exclusion and absence of deadlocks. Finally, it is shown how these decision procedures can be used to reason about certain systems with a communication network.
- 1 APT, K. R., AND KOZEN, D. Limits to automatic program verification. Inf. Proc. Lett. 22, 6 (1986), 307- 309. Google Scholar
- 2 CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. Automatic verification of finite state concurrent programs from temporal specifications. A CM Trans. Prog. Lang. Syst. 8, 2 (Apr. 1986), 244-263. Google Scholar
- 3 CLARKE, E. M., AND GRt:MBURG, O. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proceedings of 6th A CM Symposium on Principles of Distributed Computing (Vancouver, B.C., Canada, Aug. 10-12). ACM, New York, 1987, pp. 294-303. Google Scholar
- 4 CLARKE, E. M., GRUMBERG, O., AND BROWNE, M. Reasoning about networks with many identical finite state processes. In Proceedings of 5th A CM Symposium on Principles of Distributed Computing (Aug.). ACM, New York, 1986, pp. 240-248. Google Scholar
- 5 EMERSON, E. A., AND LEI, C.L. Modalities for model checking: Branching time strikes back. in Proceedings of 12th A CM Symposium on Principles of Programming Languages (New Orleans, La., Jan. 14-16). ACM, New York, 1985, pp. 84-96. Google Scholar
- 6 EMERSON, E. A., AND SISTLA, A. P. Deciding full branching time logic. Inf. Cont. 61, 3 (June 1984 ), 175 - 201.Google Scholar
- 7 HALPERN, J., AND VARDI, M. The complexity of reasoning about knowledge and time. In Proceedings of the 18th A CM SIGACT Symposium on Theory of Computing (Berkeley, Calif., May 28-30). ACM, New York, 1986, pp. 304-315. Google Scholar
- 8 HOPCROFT, J. E., AND ULLMAN, J.D. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Mass., 1979. Google Scholar
- 9 KANELLAKIS, P. C., AND SMOLKA, S. A. On the analysis of cooperation and antagonasm in networks of communicating processes. In Proceedings of 4th A CM Symposium on Principles of Distributed Computing (Minaki, Ont., Canada, Aug. 5-7). ACM, New York, 1985, pp. 23-38. Google Scholar
- 10 KARMARKAR, N. A new polynomial time algorithm for linear programming. In Proceedings of the 16th ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM, New York, 1984, pp. 302-311. Google Scholar
- 11 KARP, R., AND MILLER, R. Parallel program schemata. J. Comput. Syst. Sci. 3, 4 (May I969), 167-195. Google Scholar
- 12 KOSARAJU, S.R. Decidability of reachability in vector addition systems. In Proceedings of 14th A CM Symposmm on Theory of Computing (San Fransico, Calif., May 5-7). ACM, New York, 1982, pp. 267-281. Google Scholar
- 13 KURSHAN, R. P., AND MCMILLAN, K. A structural induction theorem for processes. In Proceedings of 8th Annual A CM Symposium on Principles of Distributed Computing (Edmonton, Alberta, Canada, Aug. 14-16). ACM, New York, 1989, pp. 239-248. Google Scholar
- 14 LADNER, R.E. The complexity of problems in systems of communicating sequential processes. In Proceedmgs of 1 lth ACM Sympostum on Theory of Computing (Atlanta, Ga., Apr. 30-May 2). ACM, New York, 1979, pp. 214-222. Google Scholar
- 15 LFHMANN, N.D. Knowledge, common knowledge, and related puzztes. In Proceedings of the 3rd AnnuaI ACM Sympostunz on Pruzctples of Dismbuted Computing (Vancouver, B.C., Canada, Aug. 27-29). ACM, New York, 1984, pp. 62-67. Google Scholar
- 16 LICI-IENSTEIN, 0., AND PNUELt, A. Checking that finite-state concurrent programs satisfy their linear specification. In Proceedings of 12th ACM Annual Symposium on Prmciples of Prograrnming Languages (New Orleans, La., Jan. 14-16). ACM, New York, 1985, pp. 97-t07. Google Scholar
- 17 LIPTON, R. The reachabllity problem requires exponential space. Re. Rep. 62, Dept. of Computer Science, Yale Univ., January, 1976.Google Scholar
- 18 MANNA, Z., AND PNUELI, A. Specification and verification of concurrent programs by v-automata. In Proceedings of 14th Annual ACM Symposium on Principles of Programming Languages (Mumch, West Germany, Jan. 21-23). ACM, New York, 1987, pp. 1-12. Google Scholar
- 19 MAYR, E. An algorithm for the general petri net teachability problem. In Proceedings of 13th Annual ACM Symposium on Theory of Computing. (Milwaukee, Wis., May 11-13). ACM, New York, 1981, pp. 238-246. Google Scholar
- 20 MILNER, R. A calculus of communicating systems. In Lecture Notes in Computer Science, Vol. 92. Springer-Verlag, New York, 1980. Google Scholar
- 21 PAPADIMITRIOU, C. H., AND STEIGLITZ, K. Combinatorial Optimization: Algorlthms and Complexity. Prentice-Hall, Englewood Cliffs, N.J., 1982. Google Scholar
- 22 PET~RSON, J. Petri Net Theory and the Modeling of Systems Prentice-Hall, Englewood Cliffs, N.J., 1981. Google Scholar
- 23 PETRI, C. Fundamentals of a theory of asynchronous information flow. In bzformatzon Processing 62, Proceedings of the 1962 IFIP Congress. North-Holland, Amsterdam, The Netherlands, 1962, pp. 386-390.Google Scholar
- 24 RACKOW, C. The covering and boundedness problem for VAS. Theoret. Comput. Sci. 6 (1978) 223-231.Google Scholar
- 25 REIF, J., AND SISTLA, A.P. A multiprocess network logic with temporal and spatial modalities. J. Comput. Syst. Sei. 30, 1 (Feb 1985), 41-53. Google Scholar
- 26 ROSmR, L., AND YEN, H. A multi-parameter analysis of the boundedness problem for VAS. J. Comput. Syst. Sci. 32 (1986), 105-135. Google Scholar
- 27 SAVITCH, W.J. Relationship between non-deterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 2 (1970), 177-192.Google Scholar
- 28 SISTLA, A. P. Theoretical issues in the design and verification of distributed systems. Ph.D. d~ssertation. Harvard Univ., Cambridge, Mass. 1983. Google Scholar
- 29 SrSTLA, A. P., ANY CLARKE, E.M. The complexity of propositional linear temporal logics. J. ACM 32 (1985), 733-749. Google Scholar
- 30 SISTLA, A. P., AND GERMAN, S.M. Reasoning with many processes. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (June). IEEE, New York, 1987, pp. 138-152.Google Scholar
- 31 SISTLA, A. P., AND GERMAN, S. M. Reasoning with many processes Tech. Note. GTE Laboratories, Inc., 1987, (available on request from the authors).Google Scholar
- 32 SISTLA, A. P., VARDI, M., AND WOLPER, P. Complementation problem for Buchi automaton and its applications to temporal logic. Theoret. Comput. Sci. 49, 2, 3 (1987), 217-237. Google Scholar
- 33 VARD~, M., AND WOLPER, P. An automata theoretic approach to automatic program verification. In Proceedings of 1st IEEE Symposium on Logic in Computer Science (June). IEEE, New York, 1986.Google Scholar
- 34 VARDZ, M., WOLPER, P., AND SISTLA, A. P. Reasoning about infinite computation paths. I n Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (Tucson, Az.). IEEE, New York, 1983, pp. 185-194.Google Scholar
- 35 WOLPER, P., AND LOVXNFOSSE, V. Verifying properties of large sets of processes with network invariants (preliminary Draft). In Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems. Grenoble, France, June, 1989. Google Scholar
Index Terms
- Reasoning about systems with many processes
Recommendations
Model checking of systems with many identical timed processes
Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, lossy channel ...
Synthesis of concurrent systems with many similar processes
Methods for synthesizing concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these ...
Counting dynamically synchronizing processes
We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared ...
Comments