How to determine and use place flows in coloured Petri nets

The theory behind the notions of place invariants and place flows for coloured Petri nets has been known since 1980, but the lack of tool support entails that the practical use of these results has been very limited. The aim of this paper is to help bridging the gaps between the theory and tool support related to place flows, and in this way support the practical use of place flows. There are three related problem areas to attack: finding place flows from the structure and inscriptions of CP-nets, showing how the place flows determine place invariants, and finally finding properties of CP-nets from the place invariants. We show how checking that a set of weights determines a place flow can be formulated as a λ-expressions rewriting problem, allowing us to use the whole set of techniques developed inside the field of λ-calculus. We also show how these techniques can be used to prove properties such as deadlock-freeness.