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.




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