In: Ajmone Marsan, M.: Lecture Notes in Computer Science, Vol. 691; Application and Theory of Petri Nets 1993, Proceedings 14th International Conference, Chicago, Illinois, USA, pages 262-281. Springer-Verlag, 1993.
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.