Petri nets with individual tokens (Q1083212)

In the well-known model of Petri nets (place/transition nets), actual system states are represented as distributions of 'black' tokens on the places on the nets. Such tokens cannot be identified as individual objects. The introduction of individual objects as tokens considerably increases the descriptive power of nets and allows for small but efficient models of real systems. This paper presents such nets and illuminates their mathematical background. Our central concern is an intuitively and mathematically simple and transparent calculus of invariants, i.e., a powerful analysis technique. Other models of nets with individual tokens, viz. Predicate/Transition nets and coloured nets, will be translated to our calculus. In this way our invariant techniques become applicable to those models.