Petri Nets With Individual Tokens

In the well known model of Petri nets (place/transition-nets), actual system states are represented as distributions of “black” tokens onto the places of the nets. Such tokens can not be identified as individual objects. The introduction of individual objects as tokens increases considerably the descriptive power of nets and allows for small but efficient models of real systems.This paper presents a calculus of such nets. We introduce its formal basis (a module of multirelations) and derive S- and T-invariants as analysis tools.Finally we compare our calculus with the predicate/transition-net model of Genrich and Lautenbach and the coloured net model of Jensen.