Relabelling LTS for Petri Net Synthesis via Solving Separation Problems

Petri net synthesis deals with finding an unlabelled Petri net with a reachability graph isomorphic to a given usually finite labelled transition system (LTS). If there is no solution for a synthesis problem, we use label splitting. This means that we relabel edges until the LTS becomes synthesisable. We obtain an unlabelled Petri net and a relabelling function, which together form a labelled Petri net with the original, intended behaviour. By careful selection of the edges to relabel we hope to keep the alphabet of the LTS and the constructed Petri net as small as possible. Even approximation algorithms, not yielding an optimal relabelling, are hard to come by. Using region theory, we develop a polynomial heuristic based on two kinds of separation problems. These either demand distinct Petri net markings for distinct LTS states or a correspondence between the existence of an edge in the LTS and the activation of a transition under the state’s marking. If any separation problem is not solvable, relabelling of edges in the LTS becomes necessary. We show efficient ways to choose those edges