Technical reports

Extending coloured petri nets

Jonathan Billington

September 1988, 82 pages

DOI: 10.48456/tr-148

Abstract

Jensen’s Coloured Petri Nets (CP-nets) are taken as the starting point for the development of a specification technique for complex concurrent systems. To increase its expressive power CP-nets are extended by including capacity and inhibitor functions. A class of extended CP-nets, known as P-nets, is defined that includes the capacity function and the threshold inhibitor extension. The inhibitor extension is defined in a totally symmetrical way to that of the usual pre place map (or incidence function). Thus the inhibitor and pre place maps may be equated by allowing a marking to be purged by a single transition occurrence, useful when specifying the abortion of various procedures. A chapter is devoted to developing the theory and notation for the purging of a place’s marking or part of its marking.

Two transformations from P-nets to CP-nets are presented and it is proved that they preserve interleaving behaviour. These are based on the notion of complementary places defined for PT-nets and involve the definition and proof of a new extended complementary place invariant for CP-nets

The graphical form of P-nets, known as a P-Graph, is presented formally and draws upon the theories developed for algebraic specification. Arc inscriptions are multiples of tuples of terms generated by a many-sorted signature. Transition conditions are Boolean expressions derived from the same signature. An interpretation of the P-Graph is given in terms of a corresponding P-net. The work is similar to that of Vautherin but includes the inhibitor and capacity extension and a number of significant differences. in the P-Graph concrete sets are associated with places, rather than sorts and likewise there are concrete initial marking and capacity functions. Vautherin associates equations with transitions rather than the more general Boolean expressions. P-Graphs are useful for specification at a concrete level. Classes of the P-Graph, known as Many-sorted Algebraic Nets and Many-sorted Predicate/Transition nets, are defined and illustrated by a number of examples. An extended place capacity notation is developed to allow for the convenient representation of resource bounds in the graphical form.

Some communications-oriented examples are presented including queues and the Demon Game of international standards fame.

The report concludes with a discussion of future work. In particular, an abstract P-Graph is defined that is very similar to Vautherin’s Petri net-like schema, but including the capacity and inhibitor extensions and associating boolean expressions with transitions. This will be useful for more abstract specifications (eg classes of communications protocols) and for their analysis.

It is believed that this is the first coherent and formal presentation of these extensions in the literature.

Full text

PDF (3.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-148,
  author =	 {Billington, Jonathan},
  title = 	 {{Extending coloured petri nets}},
  year = 	 1988,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-148.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-148},
  number = 	 {UCAM-CL-TR-148}
}