Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond

TL;DR

This paper introduces new polynomial-time algorithms for synthesizing Weighted Marked Graphs and Choice-Free Petri nets from circular labeled transition systems, expanding the theoretical understanding and practical methods for net synthesis.

Contribution

The paper provides new conditions and two efficient algorithms for synthesizing WMGs from circular LTSs, and extends some results to CF nets with three-letter alphabets.

Findings

New polynomial-time synthesis algorithms for WMGs.

Conditions for WMG existence based on circular LTSs.

Extension of conditions to CF nets with three-letter alphabets.

Abstract

In previous studies, several methods have been developed to synthesise Petri nets from labelled transition systems (LTS), often with structural constraints on the net and on the LTS. In this paper, we focus on Weighted Marked Graphs (WMGs) and Choice-Free (CF) Petri nets, two weighted subclasses of nets in which each place has at most one output; WMGs have the additional constraint that each place has at most one input. We provide new conditions for checking the existence of a WMG whose reachability graph is isomorphic to a given circular LTS, i.e. forming a single cycle; we develop two new polynomial-time synthesis algorithms dedicated to these constraints: the first one is LTS-based (classical synthesis) while the second one is vector-based (weak synthesis) and more efficient in general. We show that our conditions also apply to CF synthesis in the case of three-letter alphabets, and we discuss the difficulties in extending them to CF synthesis over arbitrary alphabets.