  This paper considers the liveness enforcement problem in a class of Petri
nets (PNs) modeling distributed systems called Synchronized Sequential
Processes (SSP). This class of PNs is defined as a set of mono-marked state
machines (sequential machines, called also agents) cooperating in a distributed
way through buffers. These buffers could model intermediate products in a
production system or information channel in a healthcare system but they should
be destination private to an agent. The designed controller for liveness
enforcement should preserve this important property characteristic to the
distributed systems. The approach in this paper is based on the construction of
a control PN that is an abstraction of the relations of the T-semiflows and
buffers. The control PN will evolve in parallel with the system, avoiding the
firing of transitions that may lead the system to livelock. An algorithm to
compute this control PN is presented. Moreover, in order to ensure the liveness
of control PN, another algorithm is proposed allowing the firing of local
T-semiflow in the correct proportion. Finally, an algorithm for guiding the
system evolution is also proposed.
