A really abstract concurrent model and its temporal logic

ABSTRACT

In this paper we advance the radical notion that a computational model based on the <i>reals</i> provides a more abstract description of concurrent and reactive systems, than the conventional <i>integers</i> based behavioral model of execution <i>sequences.</i> The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a <i>fully abstract</i> temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of <i>finite variability,</i> we achieve a balanced formalism that is insensitive to <i>finite</i> stuttering, but can recognize <i>infinite</i> stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.

REFERENCES

• 1: Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984 [doi>10.1145/800057.808665]
• 2: {BKP2} Barringer, H., Kuiper, R., Pnueli, A. --- A Compositional Temporal Approach to a CSP-like Language, Proc. of IFIP Conference: The Role of Abstract Models in Information Processing, Vienna (1985).
• 3: J. W. de Bakker , John-Jules Ch. Meyer , Ernst-Rüdiger Olderog, Infinite Streams and Finite Observations in the Semantics of Uniform Concurrency, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.149-157, July 15-19, 1985
• 4: Stephen D. Brookes, A Semantics and Proof System for Communicating Processes, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.68-85, June 06-08, 1983
• 5: {Bu} Burgess, J. P. --- Basic Tense Logic, in D. Gabbay and F. Guenthner (eds.) Handbook of Philosophical Logic, Vol II, D. Reidel Publishers (1984) 89--133.
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: Edmund M. Clarke , Bud Mishra, Automatic Verification of Asynchronous Circuits, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.101-115, June 06-08, 1983
• 8: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 9: {HO} Hailpern, B., Owicki, S. --- Modular Verification of Computer Communication Protocols, <i>IEEE Trans. on Communications,</i> COM-31, <b>1</b> (1983) 56--68.
• 10: {HP} Hennesy, M.C.B., Plotkin, G. D. --- Full Abstraction for a Simple Parallel Programming Language, Mathematical Foundations of Computer Science, <i>LNCS,</i> <b>74,</b> Springer Verlag (1979) 108--120.
• 11: Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 12: {La1} Lamport, L. --- What Good is Temporal Logic?, Proc. IFIP Congress, Paris (1983) 657--668.
• 13: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 14: {LP} Lichtenstein, O., Pnueli, A. --- A Deductive System for the Temporal Logic of the Reals, Technical Report, Weizmann Institute of Science, in preparation.
• 15: Orna Lichtenstein , Amir Pnueli , Lenore D. Zuck, The Glory of the Past, Proceedings of the Conference on Logic of Programs, p.196-218, June 17-19, 1985
• 16: {M1} Milner, R. --- Fully Abstract Models of Typed &gamma;-Calculi, Theoretic Computer Science (1977).
• 17: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 18: {MP1} Manna, Z., Pnueli, A. --- Verification of Concurrent Programs: The Temporal Framework, in Correctness Problem in Computer Science, R. S. Boyer, J. S. Moore (eds.) Academic Press (1982) 215--273.
• 19: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 20: {MP3} Manna, Z., Pnueli, A. --- Verification of Concurrent Programs: A Temporal Proof System, Foundations of Computer Science IV, Distributed Systems, <i>Mathematical Centre Tracts,</i> <b>159</b>, Amsterdam (1983) 163--255.
• 21: Rocco De Nicola , Matthew Hennessy, Testing Equivalence for Processes, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.548-560, July 18-22, 1983
• 22: Van Nguyen , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.121-131, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318624]
• 23: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 24: {Pe} Peterson G. L. --- Myths about the Mutual Exclusion Problem, <i>Information Processing Letters</i> <b>12,</b>3 (1981) 115--116.
• 25: {Pn1} Pnueli, A. --- The Temporal Semantics of Concurrent Programs, <i>Theoretical Computer Science</i> <b>13</b> (1981) 45--60.
• 26: {Pn2} Pnueli, A. --- In Transition from Global to Modular Temporal Reasoning About Programs, Proc of NATO School on Logic and Models for Verification and Specification of Concurrent Systems, La Colle-Sur-Loup (1984).
• 27: {SMS} Schwartz, R. L., Melliar-Smith, P. M. --- Temporal Logic Specifications of Distributed Systems, 2nd International Conference on Distributed Computing Systems, Paris (1981).