In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 73-92. Springer-Verlag, June 1996.
Abstract: This paper deals with the compositionality of liveness when synchronizing two colored FIFO nets. The composition operator allows to merge transitions as well as some adjacent places or queues. A behavioral sufficient condition for liveness compositionality relies on a mutual non constraining relation between component nets. A structural sufficient condition for synchronization preserving liveness is then considered in the case of a state machine at the interface of the merged elements with the non merged ones of each component net. It requires that the conflictual colored transitions of the interface state machines satisfy the structural freeing or blocking relations. Finally an example shows how these conditions simplify the analysis of a protocol within a layered architecture.
Keywords: blocking relation; colored FIFO nets; compositionality; equal conflict; freeing relation; liveness; state machine; synchronization; synchronization medium.
Back to the Petri Nets Bibliography