Synthesizing Petri Nets from Labelled Petri Nets using Token Trail Regions

Abstract

Synthesis automatically generates a process model from a behavioural specification. When the target model is a Petri net, we address synthesis through region theory. Researchers have studied region-based synthesis extensively for state-based specifications, such as transition systems and step-transition systems, as well as for language-based specifications. Accordingly, in literature, region theory is divided into two main branches: state-based regions and language-based regions. Using state-based regions, the behavioural specification is a set of global states and related state-transitions. This representation can express conflicts and the merging of global states naturally. However, it suffers from state explosion and can not express concurrency explicitly. Using language-based regions, the behavioural specification is a set of example runs defined by partially or totally ordered sets of events. This representation can express concurrency and branching naturally. However, it grows rapidly with the number of choices and can not express merging of conflicts. So far, synthesis requires a trade-off between these two approaches. Both region definitions have fundamental limitations, and synthesis therefore always involves a compromise. In this paper, we lift these limitations by introducing a new region theory that covers both state-based and language-based input. We prove that the new definition is a region meta theory that combines both concepts. It uses specifications given as a set of labelled nets, which allow us to express conflicts, concurrency and merging of local states naturally, and synthesizes a Petri net that simulates all labelled nets of the input specification.