Formal Definition of Coloured Petri Nets

  • Kurt Jensen
Part of the EATCS Monographs in Theoretical Computer Science book series (EATCS)


This chapter contains the formal definition of non-hierarchical CP-nets and their behaviour. A non-hierarchical CP-net is defined as a many-tuple. However, it should be understood that the only purpose of this is to give a mathematically sound and unambiguous definition of CP-nets and their semantics. Any concrete net, created by a modeller, will always be specified in terms of a CPN diagram (i.e., a diagram similar to Figs. 1.7 and 1.13) — or by a hierarchical CPN diagram (to be introduced in Chap. 3). It is in principle (but not in practice) easy to translate a CPN diagram into a CP-net tuple, and vice versa. The tuple form is adequate when we want to formulate general definitions and prove theorems which apply to all (or a large class) of CP-nets. The graph form is adequate when we want to construct a particular CP-net modelling a specific system.


Formal Definition Occurrence Sequence Token Colour Resource Allocation System Reachable Marking 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Kurt Jensen
    • 1
  1. 1.Computer Science DepartmentAarhus UniversityAarhus CDenmark

Personalised recommendations