Synthesis of Petri Nets from Labelled Transition Systems

The focus now shifts from analysing the behavioural properties of a given Petri net to synthesising a Petri net from a given behavioural specification. Behavioural specifications are going to be captured formally as labelled transition systems. Such transition systems are very much akin to the reachability graph of a Petri net. Labelled transition systems are often used, quite independently of Petri nets, as specifications in many different contexts. We will now – and in the next chapters – consider a labelled transition system to be given, and we will investigate whether a Petri net can be synthesised from it, and if so, how this can be done algorithmically. The idea is that a labelled transition system specifies some desired behaviour which is then realised by a – hopefully much smaller and more concurrent – Petri net.