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>

Transition Systems, Event Structures and Unfoldings

<p>Elementary transition systems were introduced by the authors in DAIMI PB-310. They were proved to be, in a strong categorical sense, the transition system version of elementray net systems. The question arises whether the notion of a region and the axioms (mostly based on regions) imposed on ordinary transition systems to obtain elementray net systems. Stated differently, one colud ask whether elementray transition systems could also play a role in characterizing other models of concurrency.</p><p> </p><p>We show here that by smoothly stengthening the axioms of elementary transition systems one obtains a subclass called occurrence transitions systems which turn out to be categorically equivalent to the well-known model of concurrency called prime event structures.</p><p> </p><p>Next we show that occurrence transition systems are to elementry transition systems what occurrence nets are to elementary nets systems. We define an ''unfold'' operation on elementry transition systems which yields occurrence transistion systems. We then prove that this operation uniquely extends to a functor which is the right adjoint to the inclusion functor from (the full subcategory of) occurrence transition systems to (the category of) elementary transition systems. Thus the results of this paper also show that the semantic theory of elementray net systems has a nice counterpart in the more abstract world of transition systems.</p>