# Sometimes ‘some’ is as good as ‘all’

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- [1]B. Alpern, F.B. Schneider, Defining Liveness, Information Processing Letters 21, 1985, 181–185.zbMATHMathSciNetCrossRefGoogle Scholar
- [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]J. W. deBakker, Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, N. J., 1980.Google Scholar
- [4]H. Barringer, R. Kuiper, A. Pnueli, Now You May Compose Temporal Logic Specification, Proceedings of 16
^{th}ACM Symposium on Theory of Computing, 1984, 51–63.Google Scholar - [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]E. Chang, Z. Manna, A. Pnueli, The Safety-Progress Classification, Manuscript 1992.Google Scholar
- [7]M. Clint, Program proving: Coroutines, Acta Informatica 2, 1973, 50–63.CrossRefGoogle Scholar
- [8]Tz. Elrad, N. Francez, Decomposition of Distributed Programs into Communication-Closed Layers, Science of Computer Programming 2 (1982), 155–173zbMATHCrossRefGoogle Scholar
- [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]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]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]D. Harel, First order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, 1979.Google Scholar
- [13]C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.Google Scholar
- [14]W. Janssen, J. Zwiers, Protocol Design by Layered Decomposition, A compositional Approach, 2
^{nd}Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, The Netherlands, 1992, LNCS 571, Springer-Verlag, 307–326.Google Scholar - [15]S. Katz, D. Peled, Interleaving Set Temporal Logic, Theoretical Computer Science 75 (1990), 21–43.MathSciNetCrossRefGoogle Scholar
- [16]S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, to appear in Distributed Computing.Google Scholar
- [17]M. Z. Kwiatkowska, Fairness for Non-interleaving Concurrency, Phd. Thesis, Faculty of Science, University of Leicester, 1989.Google Scholar
- [18]“Sometime” is Sometimes “Not Never” — On the Temporal Logic of Programs, Proceedings of the 7
^{th}ACM symposium on Principles of Programming Languages, 1980, 174–185.Google Scholar - [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]Z. Manna, A. Pnueli, Completing the temporal picture, Theoretical Computer Science 83 (1991), 97–130.zbMATHCrossRefGoogle Scholar
- [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]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]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]D. Peled, M. Joseph, A Compositional Approach to Fault Tolerance Using Specification Transformation, Manuscript, 1992.Google Scholar
- [25]D. Peled, A. Pnueli, Proving partial order liveness properties, in M.S. Paterson (ed.), Proceedings of the 17
^{th}ICALP, LNCS 443, Springer-Verlag, 1990, 553–571.Google Scholar - [26]W. Penczek, A Concurrent Branching Time Temporal Logic, Conference on Computer Science Logic, LNCS 440, Springer-Verlag, 1989, 337–354.Google Scholar
- [27]S. Pinter, P. Wolper, A Temporal Logic for Reasoning about Partially Ordered Computations, Proceedings of the 3
^{rd}ACM Symposium on Principles of Distributed Computing, Vancouver, B. C., August 1984, 23–27.Google Scholar - [28]A. Pnueli, The Temporal Logic of Programs, Proceedings of the 18
^{th}Symposium on Foundation of Computer Science, IEEE, Providence, 1977, 46–57.Google Scholar - [29]F. A. Stomp, W. P. deRoever, Designing Distributed Algorithms by Means of Formal Sequentially Phased Reasoning, Proceedings of the 3
^{rd}International Workshop on Distributed Algorithms, LNCS 392, Springer-Verlag, 1989, 242–253.Google Scholar - [30]A. Valmari, Stubborn Sets for Reduced State Space Generation, 10
^{th}International Conference on Application and Theory of Petri Nets, Germany, 1989, Vol 2, 1–22.Google Scholar - [31]J. Zwiers, Compositionality, Concurrency and Partial Correctness, LNCS 321, Springer-Verlag, 1987.Google Scholar
- [32]L. Zhiming, M. Joseph, Transformations of programs for fault-tolerance, to appear in Formal Aspects of Computing.Google Scholar