Abstract
Modular design principles have gained great importance for the development of distributed systems. Compositional system properties are regarded as technical foundation for modular design methods. This paper introduces a compositional operator “changes to” for the expression of liveness properties, where the notion of composition is formalized by merging of places of Petri nets. “Changes to” is one operator of a temporal proof calculus which combines Petri nets with a UNITY-like temporal logic. The logic is interpreted on partial order semantics of Petri nets which allows the formalization of progress in distributed systems without a global fairness assumption.
In order to apply the operator “changes to” for proving a property of an example system, we introduce some additional operators and a part of the proof calculus.
supported by the Deutsche Forschungs Gemeinschaft SFB 342, TP A3: SEMAFOR.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
J. Desel, D. Gomm, E. Kindler, B. Paech, and R. Walter. Bausteine eines kompositionalen Beweiskalküls für netzmodellierte Systeme. SFB-Bericht Nr. 342/16/92 A, Technische Universität München, July 92.
Ekkart Kindler. Invariants, compositionality, and substitution. SFB-Bericht Nr. 342/25/92 A, Technische Universität München, November 1992.
Shmuel Katz and Doron Peled. Interleaving set temporal logic. Theoretical Computer Science, 75:263–287, 1990.
Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, March 1977.
Leslie Lamport. A temporal logic of actions. Research Report SRC57, Digital Equipment Corporation, Systems Research Center, April 1990.
M. Mukund and P.S. Thiagarajan. An axiomatization of event structures. LNCS 405, pages 143–160. Springer, 1989.
Barbara Paech. Concurrency as a modality. SFB-Bericht Nr. 342/1/91 A, Technische Universität München, Institut für Informatik, January 1991.
Barbara Paech. Extending temporal logic by explicit concurrency. In MFCS, LNCS 520, pages 377–386. Springer, 1991.
David Peleg. Concurrent dynamic logic. Journal of the ACM, 34(2):450–479, 1987.
W. Penczek. A temporal logic for event structures. Fundamenta Informaticae, 11:297–326, 1988.
Amir Pnueli. Specification and development of reactive systems. In H.-J. Kugler, editor, Information Processing, pages 845–858. IFIP, Elsevier Science Publishers B.V. (North-Holland), 1986.
Shlomit S. Pinter and Pierre Wolper. A temporal logic for reasoning about partially ordered computations. In Proceedings Third Symposium on Principles of Distributed Computations, pages 28–37. ACM, August 1984.
Wolfgang Reisig. Petri Nets, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
Wolfgang Reisig. Towards a temporal logic for causality and choice in distributed systems. In REX workshop, LNCS 354, pages 603–627. Springer, 1988.
Wolfgang Reisig. Parallel composition of liveness. SFB-Bericht Nr. 342/30/91 A, Technische Universität München, 1991.
Beverly A. Sanders. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing, 3:189–205, 1991.
P.S. Thiagarajan. Elementary net systems. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Central Models and Their Properties, LNCS 254, Pages 26–59. Springer-Verlag, September 1986.
Walter Vogler. Failure semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139–162, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gomm, D., Kindler, E., Paech, B., Walter, R. (1993). Compositional liveness properties of EN-systems. In: Ajmone Marsan, M. (eds) Application and Theory of Petri Nets 1993. ICATPN 1993. Lecture Notes in Computer Science, vol 691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56863-8_51
Download citation
DOI: https://doi.org/10.1007/3-540-56863-8_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56863-6
Online ISBN: 978-3-540-47759-4
eBook Packages: Springer Book Archive