When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Reversible computation deals with mechanisms for undoing the effects of actions executed by a dynamic system. This paper is concerned with reversibility in the context of Petri nets which are a general formal model of concurrent systems. A key construction we investigate amounts to adding ‘reverse’ versions of selected net transitions. Such a static modification can severely impact on the behaviour of the system, e.g., the problem of establishing whether the modified net has the same states as the original one is undecidable. We therefore concentrate on nets with finite state spaces and show, in particular, that every transition in such nets can be reversed using a suitable set of new transitions.

A word is called Petri net solvable if it is isomorphic to the reachability graph of an unlabelled Petri net. In this paper, the class of finite, two-letter, Petri net solvable words is studied. A linear time, necessary condition allows for an educated guess at which words are solvable and which are not. A full decision procedure with a time complexity of \(O(n^2)\) can be built based on letter counting. The procedure is fully constructive and can either yield a Petri net solving a given word or determine why this fails. Algorithms solving the same problem based on systems of integer inequalities reflecting the potential Petri net structure are only known to be in \(O(n^3)\) . Finally, the decision procedure can be adapted from finite to cyclic words.