Petri net models for algebraic theories of concurrency

In this paper we discuss the issue of interleaving semantics versus True concurrency in an algebraic setting. We present various equivalence notions on Petri nets which can be used in the construction of algebraic models:(a)the occurrence net equivalence of Nielsen, Plotkin & Winskel;(b)bisimulation equivalence, which leads to a model which is isomorphic to the graph model of Baeten, Bergstra & Klop;(c)the concurrent bisimulation equivalence, which is also described by Nielsen & Thiagarajan, and Goltz;(d)partial order equivalences which are inspired by work of Pratt, and Boudol & Castellani.A central role in the paper will be played by the notion of real-time consistency. We show that, besides occurrence net equivalence, none of the equivalences mentioned above (including the partial order equivalences!) is real-time consistent. Therefore we introduce the notion of ST-bisimulation equivalence, which is real-time consistent. Moreover a complete proof system will be presented for those finite ST-bisimulation processes in which no action can occur concurrently with itself.