Skip to main content
SpringerLink
Log in

Interleaving set temporal logic

  • Collected Papers
  • Conference paper
  • First Online:
Book cover Temporal Logic in Specification

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 398))

Abstract

A new temporal logic and interpretation are suggested which have features from linear temporal logic, branching time temporal logic, and partial order temporal logic. The new logic can describe properties essential to the specification and correctness proofs of distributed algorithms such as those for global snapshots. It is also appropriate for the justification of proof rules and ascribing temporal semantics to properties such as layering of a program. These properties cannot be described with existing temporal logics. The semantic model of the logic is based on a collection of sets of interleaving sequences which reflect partial orders from the underlying semantics of the computational model. For the common partial order derived from sequentiality in execution of each process, the logic will distinguish between nondeterminism due to the parallel execution and nondeterminism due to local nondeterministic choices. The difference in expressive power is thus qualitative, and not merely due to the presence or absence of a particular temporal operator. In the logic, theorems are proven which clarify when it is possible to establish a property P for some of the interleaving computations, and yet conclude the truth of P for every interleaving.

A preliminary version of this work appeared in the Proceedings of the Sixth ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, August 1987, pages 178–190.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Abrahamson, Decidability and expressiveness of logics of programs, Ph.D. thesis, University of Washington at Seattle, 1980.

    Google Scholar 

  2. K.R. Apt, N. Francez, S. Katz, Appraising fairness in languages for distributed programming, 14th Symposium on principles of programming languages, Munich, West Germany, 1987.

    Google Scholar 

  3. K.R. Apt, N. Francez, W.P. de Roever, A proof system for Communicating Sequential Processes, ACM TOPLAS Vol 2(1980), 359–385.

    Google Scholar 

  4. M. Ben-Ari, Z. Manna, A. Pnueli, The temporal logic of branching time, Acta informatica 20(1983), 207–226.

    Google Scholar 

  5. E. Best, B. Randell, A formal model of atomicity in asynchronous systems, Acta informatica, 16(1981), 93–124.

    Google Scholar 

  6. G. Boudol, I. Castellani, On the semantics of concurrency: Partial orders and transition systems. In: proceeding TAPSOFT 87,Lecture Notes in Computer Science, Springer-Verlag, 249, 123–137.

    Google Scholar 

  7. L. Bouge, Repeated snapshots in synchronous systems and their implementation in CSP, Tech. Rep. No 84, L.I.T.P., Universite Paris 7, Paris, October 1985.

    Google Scholar 

  8. K.M. Chandy, L. Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems, Vol. 3, No. 1, 63–75.

    Google Scholar 

  9. E.M. Clarke, E.A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logics of programs Workshop, Yorktown Heights, New York, 1981, Lecture Notes in Computer Science, Springer-Verlag, 131, 52–71.

    Google Scholar 

  10. C. Courcoubetis, M.Y. Vardi, P. Wolper, Reasoning about fair concurrent programs,Proc. 18th ACM Symposium on theory of computing, Berkeley, California, 1986, 283–294.

    Google Scholar 

  11. P. Degano, R. De Nicola, U. Montanari, Partial ordering for CCS. In: Proceeding FCT 85, Lecture Notes in Computer Science, Springer-Verlag, 199, 520–533.

    Google Scholar 

  12. E.W. Dijkstra, The distributed snapshot algorithm of K.M. Chandy and L. Lamport, EWD864a.

    Google Scholar 

  13. Tz. Elrad, N. Francez, Decomposition of distributed programs into communication-closed layers, Science of Computer Programming 2(1982), 155–173

    Google Scholar 

  14. E.A. Emerson, Alternative semantics for temporal logic, Theoretical Computer Science 26(1983), 121–130.

    Google Scholar 

  15. E.A. Emerson, J.Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time temporal logic, Journal of the ACM 33(1986), 151–178.

    Google Scholar 

  16. E.A. Emerson, J.Y. Halpern, Decision procedures and expressiveness in temporal logic of branching time, Journal of Computer and System Science, 30, 1985, 1–24.

    Google Scholar 

  17. E.A. Emerson, C.L. Lei, Temporal model checking under generalized fairness constraints, Proc. 18th Hawaii International Conference on System Sciences, 1985, 277–288.

    Google Scholar 

  18. E.A. Emerson, C.L. Lei, Modalities for model checking: Branching time strikes back, Proc. 12th ACM Symposium on principles of programming languages, New Orleans, Louisiana, 1985, 84–96.

    Google Scholar 

  19. N. Francez, Fairness, texts and monographs in computer science (D. Gries, ed.), Springer-Verlag, New York, 1986.

    Google Scholar 

  20. [HS]E.C.R. Hehner, R.K. Shyamasundar, An implementation of P and V, Information Processing Letters, 12(1981), 196–198.

    Google Scholar 

  21. M.P. Herlihy, J.M. Wing, Axioms for concurrent objects, Fourteenth Symposium on Principles of Programming Languages, Munich, W.Germany, 1987, 13–26.

    Google Scholar 

  22. C.A.R. Hoare, Communicating sequential processes, Communications of the ACM, 21(1978), 666–677.

    Google Scholar 

  23. Y. Kornatzki, S. Pinter, Hyper finite state systems: A hypergraph model for distributed finite systems. Technical report of the faculty of electrical engineering, Technion, Haifa, Israel, No. 586, June 1986.

    Google Scholar 

  24. L. Lamport, Paradigms for distributed programs: computing global states, In: Distributed systems — Methods and tools for specification, An advanced course, Munich, 1985, Edited by M. Paul and H.J. Siegert, Lecture notes in Computer Science, Springer-Verlag, 190, 454–468.

    Google Scholar 

  25. L. Lamport, What good is temporal logic? Proceedings of IFIP 9th world congress, Paris, France, September 1983, 657–668.

    Google Scholar 

  26. L. Lamport, On interprocess communication, Distributed computing 1(1986), 77–85.

    Google Scholar 

  27. L. Lamport, What it means for a concurrent program to satisfy a specification: why no one has specified priority, Proceedings of the 12th ACM Symposium on principles of programming languages, New Orleans, Louisiana, 1985, 78–83.

    Google Scholar 

  28. L. Lamport, Time, clocks, and the ordering of events in a distributed system, Communication of the ACM, 21(1978), 558–565.

    Google Scholar 

  29. L. Lamport, Atomicity in distributed algorithms, Manuscript, 24 Jan 1987.

    Google Scholar 

  30. D. Lehman, A. Pnueli, J. Stavi, Impartiality, justice, fairness: the ethics of concurrent termination, Proceedings of 8th ICALP, Acco, Israel, July 1981, Lecture notes in computer science, Springer-Verlag, 115 (O. Kariv and S. Even, eds.), 1981.

    Google Scholar 

  31. D. Lehman, S. Shelah, Reasoning with time and chance, Information and control 53(1982), 165–198.

    Google Scholar 

  32. Z. Manna, A. Pnueli, Verification of concurrent programs: the temporal framework, In: The correctness problem in computer science, Edited by R.S. Boyer & J.S. Moore, 1981, 215–273.

    Google Scholar 

  33. Z. Manna, A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Science of computer programming 4(1984), 257–289.

    Google Scholar 

  34. Z. Manna, A. Pnueli, How to cook a temporal proof system for your pet language, 10th Symposium on principles of programming languages, Austin, Texas, 1983, 141–154.

    Google Scholar 

  35. R. Milner, A calculus of communicating system, Lecture Notes in Computer Science, Springer-Verlag, 92.

    Google Scholar 

  36. S. Pinter and P. Wolper, A temporal logic for reasoning about partially ordered computations, Proceedings of 3rd ACM Principles of Distributed Computing, Vancouver, B.C., August 1984, 28–37.

    Google Scholar 

  37. V. Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, 15(1986), 33–71.

    Google Scholar 

  38. W. Reisig, Partial order semantics versus interleaving semantics for CSP like languages and its impact on fairness, 11th ICALP, Antwerp, Belgium, 1984, Lecture notes in Computer Science, Springer-Verlag, 172, 403–413.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technion, Haifa, Israel

    Shmuel Katz & Doron Peled

Authors
  1. Shmuel Katz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. Banieqbal H. Barringer A. Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Katz, S., Peled, D. (1989). Interleaving set temporal logic. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds) Temporal Logic in Specification. Lecture Notes in Computer Science, vol 398. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51803-7_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-51803-7_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51803-7

  • Online ISBN: 978-3-540-46811-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation