Presynthesis of bounded choice-free or fork-attribution nets (Q2304527)

Synthesis of Petri nets from labelled transition systems (LTS) aims at generating a Petri net such that its marking graph is isomorphic to the LTS. The synthesis problem asks whether such a Petri net exists. If the Petri net should satisfy some requirements, then the synthesis problem can be easier to solve, because sometimes the existence of a respective Petri net can be directly derived from properties of the LTS. It can also be harder, if no such properties are known. This contribution considers choice-free nets, which have, for each place, exactly one output transition, and fork-attribution nets, which additionally have, for each transition, exactly one input place. It was previously shown that marking graphs of choice-free nets have structural properties which can be employed for a so-called presynthesis: the LTS must enjoy these properties if the synthesis problem for choice-free nets has a solution. This paper generalizes and extends this result to fork-attribution nets and presents and analyzes a respective improved algorithm. Although fork-attribution nets are close to marked graphs (each transition has exactly one input and one output place), for which the synthesis problem is particularly simple to solve, the author convincingly argues that a similar result can only be obtained for plain fork-attribution nets (no weighted arcs).