Abstract
Which kind of properties of nonsequential systems should be considered essential for specification and abstraction purposes, is still an open problem. In this paper we discuss some particular properties such as absence of delay and various notions of concurrency. They turn out to be adequately representable in partial order semantics. The most fundamental version of Petri Nets appears to be convenient for such investigations. A (generalized) temporal logic is introduced, covering the intricate relationship among causality (sequentiality), choice and concurrency appearing in distributed systems.
Key words
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
E. Clarke, M. Browne, E. Emerson, A. Sistla: Using Temporal Logic for Automatic Verification of Finite State Systems. in: Logics and Models of Concurrent Systems. K. Apt (ed.), Springer-Verlag, pp. 3–26 (1985)
E. Allen Emerson, Edmund M. Clarke: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming 2, pp. 246–266 (1982
E. Allen Emerson, Joseph Y. Halpern: “Sometimes” and “Not Never” Revisited: On Branching versus Linear time. Principles of programming languages 83, pp. 127–140, ACM (1983)
P. Enhalbert, M. Michel: Many Sorted Temporal Logic for Multi-Process Systems.
G.E. Hughes, M.J. Cresswell: An Introduction to Modal Logic. Methuen, London & New York (1968)
Shmuel Katz, Doron Peled: Interleaving Set Temporal Logic. Proceedings of the ACM Symposium on Principles of Distributed Computation, Vancouver, B.C., (1987)
Leslie Lamport: “Sometime” is sometimes “Not Never”. On the Temporal Logic of Programs. 7th Annual ACM Symp. on Principles of Programming Languages, pp. 174–185 (1980)
Leslie Lamport: What Good is Temporal Logic? Information Processing 83, R.E.A. Mason (ed.), North Holland, IFIP, pp. 657–667 (1983)
K. Lodaya, P.S. Thiagarajan: A Modal Logic for a Subclass of Event Structures. 14th ICALP, Lecture Notes in Computer Science 267, Springer-Verlag pp. 290–303 (1987)
Zohar Manna, Pierre Wolper: Synthesis of Communicating Processes from Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, Vol. 6, No 1, pp. 68–93 (1984)
Mogns Nielsen, Gordon Plotkin, Glynn Winskel: Petri Nets, Event Structures and Domains, Part I. Theoretical Computer Science Vol. 13, No. 1, pp. 85–108 (1980)
Ernst Rüdiger Olderog, Ursula Goltz, Rob. v. Glabbeek: Combining Compositionality and Concurrency. Summary of a GMD-Workshop, Königswinter, March 1988. Gesellschaft für Mathematik und Datenverarbeitung, St. Augustin, Arbeitspapiere der GMD 320 (1988)
Carl Adam Petri: Non-sequential Processes. Gesellschaft für Mathematik und Datenverarbeitung, Interner Bericht ISF-77-5 (1977)
Shlomil S. Pinter, Pierre Wolper: A Temporal Logic for Reasoning about Partially Ordered Computations. Proceedings of the third ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, pp. 28–37 (1984)
Amir Pnueli: The Temporal Logic of Concurrent Programs. Theoretical Computer Science 13, pp. 45–60 (1981)
Amir Pnueli: Specification and Development of Reactive Systems. Information Processing 86, H. J. Kugler (ed.), North-Holland, pp. 845–858 (1986)
Wolfgang Reisig: Partial Order Semantics versus Interleaving Semantics for CSP-like Languages and its Impact on Fairness. Lecture Notes in Computer Science Vol. 172, J. Paredaens (ed.), Springer-Verlag, pp. 403–413 (1984)
Wolfgang Reisig: Towards a Temporal Logic for True Concurrency Part I: Linear Time Propositional Logic. Gesellschaft für Mathematik und Datenverarbeitung, St. Augustin, Arbeitspapiere der GMD 277 (1987)
Wolfgang Reisig: A Strong Part of Concurrency. Advances in Petri Nets 1987, Lecture Notes in Computer Science 266; G. Rozenberg (ed.), Springer-Verlag, pp. 238–272 (1987)
Wolfgang Reisig: Temporal Logic and Causality in Concurrent systems. Proceedings of CONCURRENCY 88, Hamburg. Lecture Notes in Computer Science, Springer-Verlag (1988)
Veronika Strack: Occurrence Structures: A Model of Concurrency and Choice in Systems. Gesellschaft für Mathematik und Datenverarbeitung, St. Augustin, Arbeitspapiere der GMD 328 (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reisig, W. (1989). Towards a temporal logic for causality and choice in distributed systems. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. REX 1988. Lecture Notes in Computer Science, vol 354. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013037
Download citation
DOI: https://doi.org/10.1007/BFb0013037
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51080-2
Online ISBN: 978-3-540-46147-0
eBook Packages: Springer Book Archive