Parametrized resolution of some families of linear equation systems

Validation of formal models of paralellism, such as vector-addition systems and Petri Nets, requires the calculation of nonnegative invariants. In general, these invariants are calculated by means of classical techniques of linear programming, such as the Simplexe algorithm or the Farkas’ algorithm. Unfortunately, these techniques are not applicable in the case of High level models as Colored Nets. In this paper, the authors develop a new useful method, for this kind of models. This technique is based on the resolution-in a parametrized way-of some families of linear equations systems, whose structures are identical, but that have a different number of equations and unknowns. The first equations family that they solve is of the type AëX1=ëëë=AëXn where A is an integer matrix and the unknowns {X1,...,Xn} are a set of nonnegative vectors; n is the parameter of this family. Once solutions for the system have been obtained, the authors solve two other families of equations, whose solutions provide a generative family of nonnegative invariants.