Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesizing Petri Nets from Labelled Petri Nets using Token Trail Regions

Robin Bergenthum, Jakub Kovář

TL;DR

Token trail regions provide a unifying, ILP-based framework for synthesizing Petri nets from heterogeneous behavioural specifications, including state graphs, partial orders, and labelled nets, by enforcing label-respecting token distributions across inputs. Each token trail region induces a corresponding place in the synthesis net, ensuring the resulting Petri net simulates all input nets with minimal extra behaviour, and the approach is implemented as a practical web tool using a bound $k$ to obtain finite approximations. The method bridges state-based and language-based region theory, enabling mixed-specification inputs and enhancing process discovery by preserving concurrency, conflicts, and local-state merging within a compact model. This yields a flexible, scalable approach for discovering and synthesizing analyzable Petri nets from diverse sources, with tunable precision and applicability to workflow nets and soundness considerations.

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.

Synthesizing Petri Nets from Labelled Petri Nets using Token Trail Regions

TL;DR

Token trail regions provide a unifying, ILP-based framework for synthesizing Petri nets from heterogeneous behavioural specifications, including state graphs, partial orders, and labelled nets, by enforcing label-respecting token distributions across inputs. Each token trail region induces a corresponding place in the synthesis net, ensuring the resulting Petri net simulates all input nets with minimal extra behaviour, and the approach is implemented as a practical web tool using a bound to obtain finite approximations. The method bridges state-based and language-based region theory, enabling mixed-specification inputs and enhancing process discovery by preserving concurrency, conflicts, and local-state merging within a compact model. This yields a flexible, scalable approach for discovering and synthesizing analyzable Petri nets from diverse sources, with tunable precision and applicability to workflow nets and soundness considerations.

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.
Paper Structure (7 sections, 6 theorems, 13 figures)

This paper contains 7 sections, 6 theorems, 13 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Token Trail Regions
  4. Token Trail Regions as Meta Regions
  5. Computing Token Trail Regions
  6. Process Discovery using Token Trail Regions
  7. Conclusion

Key Result

Theorem 3.2

Let $S = \{(C_1,E_1,F_1,i_1,l_1),\ldots,(C_n,E_n,F_n,i_n,l_n)\}$ be a set of marked labelled nets, let $r$ be a region in $S$. We denote $E = \bigcup_i E_i$ and $l = \bigcup_i l_i$. For every $t \in \{l(e) | e \in E\}$ we fix one $e_t \in E$ so that $l(e_t) = t$ and $in_r(e_t) = min\{in_r(e) | l(e)

Figures (13)

  • Figure 1: A Petri net model of the example workflow, used as a running example throughout the paper and exhibiting conflict, concurrency, loops, and arc weights.
  • Figure 2: A state-based specification of the example workflow, representing all reachable global states and possible state-transitions.
  • Figure 3: A language-based specification of the example workflow, representing individual executions as conflict-free runs.
  • Figure 4: A Petri net-based specification of the example workflow, representing part of the intended behaviour using labels and local states, and expressing conflict and concurrency.
  • Figure 5: A complete specification of the example workflow, combining state-based, language-based, and net-based models.
  • ...and 8 more figures

Theorems & Definitions (11)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 3.1
  • Theorem 3.2
  • Corollary 3.3
  • Theorem 3.4
  • Corollary 3.5
  • Theorem 4.1
  • ...and 1 more