Section 5: Variable Invariants Derieved From State Transformation Functions

In this section, we present results obtained from an invariant analysis that applies only to a specific class of state transformations. If all actions perform only linear state transformations of the type v' = v + c, where c is some integer constant, the state transformations are those of an ordinary Petri net and an invariant computation known for Petri nets can be applied.
In the following we present a set of computed variable invariants, such that a weighted summation performed for any state in the trace will yield the same constant value throughout the trace.Variables that do not contribute to invariants are likely to represent irregular or faulty behavior such that we list those actions separately and upfront.

List of variables that had to be excluded from the calculation of invariants

For this trace, all variables are taken into consideration, however this does not mean all of them are actually covered by some invariant!

List of variables that are not covered by any invariant

Set of computed variable invariants

The set of computed invariants is empty!