Transition System Models for Concurrency

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 step transition systems, called PN-transition systems, which describe the behaviour of Petri nets.This correspondence is formally described in terms of a coreflection between a category of PN-transition systems and a category of Petri nets.In this paper, we show that we can define subcategories of PN-transition systems whose objects are safe PN-transition systems and elementary PN-transition systems 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.We also prove that our category of elementary PN-transition systems is equivalent to the category of (sequential) elementary transition systems 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 PN-transition system and a subcategory of asynchronous transition systems which has been shown by Winskel and Nielsen to be closely linked to safe nets