Sequential and concurrent behaviour in Petri net theory

AbstractTwo ways of describing the behaviour of concurrent systems have widely been suggested: arbitrary interleaving and partial orders. Sometimes the latter has been claimed superior because concurrency is represented in a ‘true’ way; on the other hand, some authors have claimed that the former is sufficient for all practical purposes. Petri net theory offers a framework in which both kinds of semantics can be defined formally and hence compared with each other. Occurence sequences correspond to interleaved behaviour while the notion of a process is used to capture partial-order semantics.This paper aims at obtaining formal results about the relationship between various classes of processes and occurence sequences in net theory. We shall compare an axiomatic approach to the definition of processes with an inductive approach which relates processes to occurence sequences (and generalisations thereof). We shall show that, in general, axiomatic process semantics is more powerful than inductive semantics using occurence sequences. However, we shall also show that the latter can be generalised, or the former be restricted, to yield various equivalence results. The structure of the relation between sequences and processes will also be explored, exhibiting two meaningful relations, one on the sequences and one on the processes, which correspond to each other bijectively. We shall apply and simplify the theory to the practically important case of nets which are of finite synchronisation and 1-safe