E. M. Clarke
E. A. Emerson
A. P. Sistla
Abstract
We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
- 1 BEN-ARI, M., PNUELI, A., AND MANNA, Z. The temporal logic of branching time. Acta In{. 20 (1983), 207-226.Google Scholar
- 2 BARTLET, K. A., SCANTLEBURY, R. A., AND WILKINSON, P.T. A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12, 5 (1969), 260-261. Google Scholar
- 3 CLARKE, E. M., AND EMERSON, E.A. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings o{ the Workshop on Logic o{ Programs (Yorktown Heights, N.Y.), Lecture Notes in Computer Science, 131, Springer Verlag, New York, 1981. Google Scholar
- 4 EMERSON, E. A., AND CLARKE, E.M. Characterizing properties of parallel programs as fixpoints. In Proceedings of the 7th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, 85, Springer Verlag, New York, 1981. Google Scholar
- 5 EMERSON, E. A., AND HALPERN, J.Y. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. In Proceedings o{ the Annual ACM Symposium on Principles o{ Programming Languages (Austin, Tex., Jan. 1982). To appear in J. ACM. Google Scholar
- 6 EMERSON, E. A., AND CLARKE, E. M. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2 (1982), 241-266.Google Scholar
- 7 EMERSON, E. A., AND EEI, C.L. Modalities for model checking: Branching time strikes back. In Proceedings 12th ACM Symposium on Principles of Programming Languages (New Orleans, Jan. 1985), 84-95. Google Scholar
- 8 GABBAY, D., PNUELI, A., SHELAH, S., AND STAVI, J. The temporal analysis of fairness. In Proceedings 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Jan. 1980), 163-173. Google Scholar
- 9 HAILPERN, B. W. Verifying concurrent processes using temporal logic. In Lecture Notes in Computer Science, 129, Springer Verlag, New York, 1982. Google Scholar
- 10 HOARE, C. A. R. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978), 666-677. Google Scholar
- 11 LAMPORT, L. "Sometimes" is sometimes "not never." In Proceedings 7th Annual ACM Symposium on Principles o{ Programming Languages (Las Vegas, Jan. 1980), 174-185. Google Scholar
- 12 LEHMANN, D., PNUELI, A., AND STAVI, J. Impartiality, justice, and fairness: The ethics of concurrent termination. In Automata, Languages, and Programming. Lecture Notes in Computer Science 115, Springer Verlag, New York, 1981, 265-277. Google Scholar
- 13 MANNA, Z., AND PNUELI, A. Verification of concurrent programs: The temporal framework. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds., Academic Press, London, 1981, 215-273.Google Scholar
- 14 MANNA, Z., AND WOLPER, P. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6, 1 (Jan. 1984), 68-93. Google Scholar
- 15 OWlCKI, S., AND LAMPORT, L. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4, 3 (July 1982), 455-495. Google Scholar
- 16 QUIELLE, J. P., AND SIFAKIS, J. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science 137, Springer Verlag, New York, 1981, 337-350. Google Scholar
- 17 QUIELLE, J. P., AND SIFAK1S, J. Fairness and related properties in transition systems. 292, IMAG, Univ. of Grenoble, Mar. 1982.Google Scholar
- 18 SISTLA, A. P., AND CLARKE, E.M. Complexity of propositional linear temporal logics. J. ACM 32, 3 (July 1985), 733-749. Google Scholar
- 19 ZAFIROPULO, P., WEST, C., RUDIN, H., COWAN, D., AND BRAND, D. Towards analyzing and synthesizing protocols. IEEE Trans. Commun. COM-28, 4 (Apr. 1980), 651-671.Google Scholar
Index Terms
- Automatic verification of finite-state concurrent systems using temporal logic specifications
Recommendations
Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesWe give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size ...
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications
In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In ...
Comments