Bridging the gap between place- and floyd-invariants with applications to preemptive scheduling

Abstract

The notion of linear place-invariants for coloured nets is extended to sums of non-linear functions. The extension applies to such places where all tokens are removed by the occurrence of an output transition. It is shown how this covers the case of variable assignments and invariants in traditional programs. The result helps in understanding the relation of place-invariants of coloured nets in comparison with traditional Floyd-invariants of programs. In the second part the property of token clearing is introduced to the occurrence rule, showing that the results of the first part are still valid. Such types of nets are important for the modelling of fault tolerant applications.