2019/10/31 by Raymond Devillers, Devillers, Raymond, Evgeny Erofeev +3
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Methods in Verification #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1910.14387
openalex publication_date 2019/10/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In previous studies, several methods have been developed to synthesise Petri\nnets from labelled transition systems (LTS), often with structural constraints\non the net and on the LTS. In this paper, we focus on Weighted Marked Graphs\n(WMGs) and Choice-Free (CF) Petri nets, two weighted subclasses of nets in\nwhich each place has at most one output; WMGs have the additional constraint\nthat each place has at most one input. We provide new conditions for checking\nthe existence of a WMG whose reachability graph is isomorphic to a given\ncircular LTS, i.e. forming a single cycle; we develop two new polynomial-time\nsynthesis algorithms dedicated to these constraints: the first one is LTS-based\n(classical synthesis) while the second one is vector-based (weak synthesis) and\nmore efficient in general. We show that our conditions also apply to CF\nsynthesis in the case of three-letter alphabets, and we discuss the\ndifficulties in extending them to CF synthesis over arbitrary alphabets.\n