Checking that finite state concurrent programs satisfy their linear specification

ABSTRACT

We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program.

References

1. [BK] H. Barringer and R. Kuiper, A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, (1983).
2. [BMP] M. Ben-Ari, Z. Manna, A. Pnueli, The Temporal Logic of Branching Time, Acta Informatica 20 (1983) pp. 207-226.
3. [CE] E. M. Clarke, E. A. Emerson, Synthesis of Synchronization Skeletons for Branching Time Temporal Logic, Proc. of the Workshop on Logic of Programs, Yorktown Heights, NY, Springer Verlag LNCS Vol. 131 (1982).
4. [CES] E. M. Clarke, E. A. Emerson and A. P. Sistla, Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, 10th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1983.
5. [EH] E. A. Emerson, J. Y. Halpern, Sometimes and Not Never Revisited: On Branching Time Versus Linear Time, 10th ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983.
6. [EL] E. A. Emerson and C. L. Lei, Temporal Model Checking Under Generalieed Fairness Constraints, University of Texas, Austin July (1984).
7. [KVR] R. Koymans, J. Vytopil and W. P. de Roever, Real-time Programming and Asynchronous Message Passing, 2nd ACM Symposium on Principles of Distributed Computing, Montreal, Canada (1983) 187-197.
8. [L1] L. Lamport, 'Sometime' is Sometimes 'Not Never' A Tutorial on the Temporal Logic of Programs, Proc. of the 7th Annual ACM Symposium on Principles of Programming Languages , Jan. 1980.
9. [L2] L. Lamport, What good is Temporal Logic? Information Processing 1983, Proc. of the 9th IFIP Congress, R.E.A. Mason Editor, North Holland, pp. 657-668.
10. [LPS] D. Lehmann, A. Pnueli, J. Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Automata, Languages and Programming, Springer Verlag LNCS 115 (1981) pp. 265-277.
11. [MP1] Z. Manna, A. Pnueli, Verification of Concurrent Programs: The Temporal Framework, in the Correctness Problem in Computer Science, R. S. Boyer, J. S. Moore Editors, International Lecture Series in Computer Science, Academic Press (1981).
12. [MP2] Z. Manna, A. Pnueli, Proving Precedence Properties: The Temporal Way, Technical Report CS84-04, The Weiemann Institute February 1984, also a shorter version in Automata, Languages and Programming 10th Colloquium Barcelona, July, 1983, Springer Verlag LNCS 154, pp. 491-512.
13. [MP3] Z. Manna, A. Pnueli, Verification of Concurrent Programs: A Temporal Proof System, Foundations of Computer Science IV, Distributed Systems: Part 2, Semantics and Logic, J. W. DeBakker, J. Van Leeuwen Editors, Mathematical Centre Tracts 159 Amsterdam 1983, pp. 163-255.
14. [MP4] Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language, Symposium on Principles of Programming Languages , Austin, Texas (1983).
15. [QS1] J. P. Quelle, J. Sifakis, Specification and Verification of Concurrent Systems in CESAR, Proc. of the 5th International Symposium on Programming, 1981.
16. [QS2] J. P. Quelle, J. Sifakis, Fairness and Related Properties in Transition Systems, IMAG Research Report 292, Grenoble, March 1982.
17. [SC] A. P. Sistla, E. M. Clarke, The Complexity of Propositional Temporal Logic, 14th ACM Symaposium on Theory of Computing, May 1982, pp. 159-167.
18. [SP] R. Sherman and A. Pnueli, Semantic Tableau for Temporal Logic, Technical Report, CS81- 21, Weizmann Institute of Science, September (1981).
19. [ZWRCB] P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand, Towards Analyzing and Synthesizing Protocols, IEEE Transactions on Communications , Vol. COM-28, No. 4, April 1980, pp. 651-671.

Index Terms

• Computing methodologies

  • Concurrent computing methodologies

    • Concurrent programming languages

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

• Theory of computation

  • Logic

  • Models of computation

    • Computability