In: Proceedings of the 10th International Conference on Application and Theory of Petri Nets, 1989, Bonn, Germany, pages 52-73. 1989.
Also: Universidad de Zaragoza, departamento de ingenieria electrica e informatica, Research Report 89-03, January 1989.
Also in: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 483; Advances in Petri Nets 1990, pages 113-145. Berlin, Germany: Springer-Verlag, 1991.
Abstract: The state equation is a linear description of the reachable markings and firing count vectors of a P/T net. It has the disadvantage that its solution space, in general, includes additional integer unreachable markings and/or unfirable vectors. As a result, the analysis of properties using this linear characterization, usually leads to necessary or sufficient conditions for satisfying it, but not both. The appearance of these spurious solutions is due to the fact that the state equation does not take into account the order in which transitions fire. The existence of methods which a priori eliminate spurious solutions of the direct state equation would bring structural verification methods closer to behavioural methods. Two elimination methods are presented here. Both are based on adding to the state equation linear restrictions which (partially) check the transition firing rule. The first consists of checking that every marking which is solution of the state equation has a sequence of predecessor markings, and that the transition firing rule holds in that sequence. The second is based on the addition of implicit places to the net which are linearly non-redundant in the net state equation. Some of these places are associated to initially marked traps, and the elimination of unreachable markings they perform is based on a well-known fact: initially marked traps remain always marked. The reasoning on structural deadlocks leads to the complementary fact: initially unmarked deadlocks remain always unmarked. In this case the linear restrictions are based on the annullation of marking variables belonging to places in the deadlock. Last but not least, another important point is the characterization by means of one single Linear Programming Problem (LPP) of those implicit places which are structurally implicit. The interesting fact here is that the theoretical complexity to solve a LPP is polynomial and the practical complexity is linear.
Keywords: linearly based characterization (of) place/transition net(s); state equation; reachable marking; linear restriction; implicit place; trap; unreachable marking; structural deadlock.