Advertisement

Sometimes ‘some’ is as good as ‘all’

  • Doron Peled
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

The representation of partial order semantics as an equivalence relation on interleaving sequences was shown to extend the expressive power of interleaving semantics. A specification formalism called existential specification is introduced in which a formula is interpreted over equivalence classes of sequences by asserting that some (at least one but not necessarily all) sequences from each equivalence class satisfy a given property. It differs from the more common universal specification, which is interpreted over all sequences in all classes. Its advantage over other formalisms that deal with partial order executions lies in its simplicity: any syntax that is defined over interleaving sequences, e.g., linear temporal logic, can be adopted. It is shown how under an appropriate semantical construction, an exact existential specification of a program (i.e., each property of the program expressed using the same formalism is a consequence of this specification) can be given. Moreover, under such a construction, no information about the program is lost by choosing exact existential specification rather than exact universal specification; it is possible to generalise, by means of a proof system, an exact existential specification into an exact universal specification. Applications of these results to achieving compositional proof rules are shown.

Keywords

Temporal Logic Proof System Linear Temporal Logic Execution Sequence Concurrent Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    B. Alpern, F.B. Schneider, Defining Liveness, Information Processing Letters 21, 1985, 181–185.zbMATHMathSciNetCrossRefGoogle Scholar
  2. [2]
    K. R. Apt, N. Francez, W.P. de Roever, A proof system for communicating sequential processes, ACM Transactions on Programming Languages and Systems, Vol 2, 1980, 359–385.zbMATHCrossRefGoogle Scholar
  3. [3]
    J. W. deBakker, Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, N. J., 1980.Google Scholar
  4. [4]
    H. Barringer, R. Kuiper, A. Pnueli, Now You May Compose Temporal Logic Specification, Proceedings of 16th ACM Symposium on Theory of Computing, 1984, 51–63.Google Scholar
  5. [5]
    K. M. Chandy, L. Lamport, Distributed Snapshots: determining the global state of distributed systems, ACM Transactions on Computer Systems 3, 1985, 63–75.CrossRefGoogle Scholar
  6. [6]
    E. Chang, Z. Manna, A. Pnueli, The Safety-Progress Classification, Manuscript 1992.Google Scholar
  7. [7]
    M. Clint, Program proving: Coroutines, Acta Informatica 2, 1973, 50–63.CrossRefGoogle Scholar
  8. [8]
    Tz. Elrad, N. Francez, Decomposition of Distributed Programs into Communication-Closed Layers, Science of Computer Programming 2 (1982), 155–173zbMATHCrossRefGoogle Scholar
  9. [9]
    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.zbMATHMathSciNetCrossRefGoogle Scholar
  10. [10]
    D. Gabbay, The declarative past and imperative future, in: B. Banieqbal, H. Barringer, A. Pnueli (editors), Temporal Logic in Specification, LNCS 398, Springer-Verlag, 1987, 407–448.Google Scholar
  11. [11]
    P. Godefroid, P. Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, Proceedings of Computer-Aided Verification, Aalborg, Denmark, 1991.Google Scholar
  12. [12]
    D. Harel, First order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, 1979.Google Scholar
  13. [13]
    C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.Google Scholar
  14. [14]
    W. Janssen, J. Zwiers, Protocol Design by Layered Decomposition, A compositional Approach, 2nd Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, The Netherlands, 1992, LNCS 571, Springer-Verlag, 307–326.Google Scholar
  15. [15]
    S. Katz, D. Peled, Interleaving Set Temporal Logic, Theoretical Computer Science 75 (1990), 21–43.MathSciNetCrossRefGoogle Scholar
  16. [16]
    S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, to appear in Distributed Computing.Google Scholar
  17. [17]
    M. Z. Kwiatkowska, Fairness for Non-interleaving Concurrency, Phd. Thesis, Faculty of Science, University of Leicester, 1989.Google Scholar
  18. [18]
    “Sometime” is Sometimes “Not Never” — On the Temporal Logic of Programs, Proceedings of the 7th ACM symposium on Principles of Programming Languages, 1980, 174–185.Google Scholar
  19. [19]
    Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language. Proceedings of the Symposium on Principles on Programming Languages, Austin, Texas, 1983, 141–151.Google Scholar
  20. [20]
    Z. Manna, A. Pnueli, Completing the temporal picture, Theoretical Computer Science 83 (1991), 97–130.zbMATHCrossRefGoogle Scholar
  21. [21]
    A. Mazurkiewicz, Traces, Histories, Graphs: Instances of a process monoid, in M. Chytil (Ed.), Mathematical Foundation of Computer Science, LNCS 176, Springer-Verlag, 1984, 115–133.Google Scholar
  22. [22]
    D. Park, On the Semantics of Fair Parallelism, in D. Biorner (ed.), Proceedings on Abstract Software Specification, LNCS 86, Springer-Verlag, 1979, 504–526.Google Scholar
  23. [23]
    D. Peled, S. Katz, and A. Pnueli, Specifying and Proving Serializability in Temporal Logic, LICS 91', Amsterdam, The Netherlands, July 1991, 232–245.Google Scholar
  24. [24]
    D. Peled, M. Joseph, A Compositional Approach to Fault Tolerance Using Specification Transformation, Manuscript, 1992.Google Scholar
  25. [25]
    D. Peled, A. Pnueli, Proving partial order liveness properties, in M.S. Paterson (ed.), Proceedings of the 17th ICALP, LNCS 443, Springer-Verlag, 1990, 553–571.Google Scholar
  26. [26]
    W. Penczek, A Concurrent Branching Time Temporal Logic, Conference on Computer Science Logic, LNCS 440, Springer-Verlag, 1989, 337–354.Google Scholar
  27. [27]
    S. Pinter, P. Wolper, A Temporal Logic for Reasoning about Partially Ordered Computations, Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, B. C., August 1984, 23–27.Google Scholar
  28. [28]
    A. Pnueli, The Temporal Logic of Programs, Proceedings of the 18th Symposium on Foundation of Computer Science, IEEE, Providence, 1977, 46–57.Google Scholar
  29. [29]
    F. A. Stomp, W. P. deRoever, Designing Distributed Algorithms by Means of Formal Sequentially Phased Reasoning, Proceedings of the 3rd International Workshop on Distributed Algorithms, LNCS 392, Springer-Verlag, 1989, 242–253.Google Scholar
  30. [30]
    A. Valmari, Stubborn Sets for Reduced State Space Generation, 10th International Conference on Application and Theory of Petri Nets, Germany, 1989, Vol 2, 1–22.Google Scholar
  31. [31]
    J. Zwiers, Compositionality, Concurrency and Partial Correctness, LNCS 321, Springer-Verlag, 1987.Google Scholar
  32. [32]
    L. Zhiming, M. Joseph, Transformations of programs for fault-tolerance, to appear in Formal Aspects of Computing.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Doron Peled
    • 1
  1. 1.Department of Computer ScienceUniversity of WarwickCoventryUK

Personalised recommendations