In: Journal of Circuits, Systems and Computers, Vol. 8, No. 1, pages 223-265. 1998.
Abstract: Liveness is a basic property that in many discrete event dynamic systems is considered essential for their correct behavior. It expresses that no action (transition in P/T models) will ever become unattainable. A polynomial time necessary condition for the existence of a live and bounded marking of a P/T net is given. This condition is shown to be also sufficient for some subclasses. The applicability of these results is extended by the use of transformation techniques that allow for their exploitation in the analysis of more general nets. Some results for the structural analysis of actual liveness are also overviewed, in particular, sufficient conditions for deadlock-freeness and absence of dead transitions.
Keywords: Petri nets, linear algebra, net transformations, sequential processes.