On the analysis and synthesis of coloured Petri nets

This paper proposes an analysis and synthesis method for coloured Petri nets (CPN). We present basic CPN (paths and circuits), constituent of any CPN and determine their marking and firing invariants; subsequent properties (boundedness, consistency, and liveness) are then thoroughly examined. We exhaustively detail the assembly of these basic bricks to obtain larger (real-life) models, ensuring that "good" properties are automatically preserved. This (de)composition technique is finally applied to the examples of a FIFO stock and a FMS, to validate and show the ease of use of our method and, eventually, to enable benchmarking with other analysis methods.