A formal model of programs (Q1059401)

This paper proposes another extension of Petri nets. All arcs of the net are marked either with \(+\) or -. If there are multiple arcs between a place and a transition, all of them have the same sign. Marking has the form of integers, as opposed to non-negative integers only in classical Petri nets, put into places. When a transition is fired, values of all its input places with \(+\) arcs are decremented and those with - arcs incremented. At the same time, values of all its output places with \(+\) arcs are incremented and those with - arcs decremented. The transition can be fired only when marking of its input places is sufficient, i.e. values of places with \(+\) arcs are equal or greater than numbers of the arcs involved and values of those with - arcs are equal or less than numbers of the arcs involved. Such a net may be considered a superposition of two classical Petri nets with tokens of different signs which neutralize one another if found in the same place. The authors give all necessary formal definitions including those of languages describing firing sequences. They also show equivalence of such nets to other Petri net extensions. In particular, they prove and illustrate the equivalence between their nets and Petri nets with inhibitor arcs. Then, they investigate a certain special case of their nets, which they claim well suited as a formal model of parallel programs.