Transition System Models for Concurrency

<p>Labelled transition systems can be extended to faithfully model concurrency by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step, We can characterize a subclass of these <em>step transition systems</em>, called PN-transition systems, which describe the behaviour of Petri nets.</p><p>This correspondence is formally described in terms of a coreflection between a category of <em>PN</em>-transition systems and a category of Petri nets.</p><p>In this paper, we show that we can define subcategories of <em>PN</em>-transition systems whose objects are <em> safe PN-transition systems and elementary PN-transition systems</em> such that there is a coreflection between these subcategories and subcategories of our category of Petri nets corresponding to safe nets and elementary net systems.</p><p>We also prove that our category of elementary <em>PN</em>-transition systems is equivalent to the category of (sequential) <em> elementary transition systems</em> defined by Nielsen, Rozenberg and Thiagarajan, thereby establishing that the concurrent behaviour of an elementary net system can be completely recovered from a description of its sequential behaviour. Finally, we establish a coreflection between our category of safe <em>PN</em>-transition system and a subcategory of <em>asynchronous transition systems</em> which has been shown by Winskel and Nielsen to be closely linked to safe nets.</p>