Property specification for coloured Petri nets

The coloured Petri nets is a powerful modelling framework, which allows designers to attach values of complex types (colors) to moving objects (tokens). Using analysis techniques of the classical Petri nets for the coloured Petri nets demands abstracting from colors that can be a source of errors. In this paper we propose a logic and a tool prototype to formulate properties of a coloured Petri net without abstracting from colors. These properties can be used both for checking correctness and for planning and controlling the simulation process. We show examples of properties for a simplified coloured Petri net of a distribution center.