Sequential and concurrent behaviour in Petri net theory (Q1119024)

The authors examine the interleaved (occurrence sequence) behaviour semantics and the partial-order (process) semantics and the relationships between these semantics. An axiomatic approach to the definition of processes is compared with an inductive approach which relates processes to occurrence sequences. The comparison is done in the framework of Petri nets, because both types have already been formalized in different ways in net theory. The question of the `right' set of axioms is discussed, and whether (and when) process semantics is more powerful than occurrence sequence semantics. To every theory, the full formal proof is given.