Compositional liveness properties of en-systems

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.