2026-07-22T19:23:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7780 2024-03-06T10:41:06Z ddc:004 open_access

k-Bounded Petri Net Synthesis from Modal Transition Systems Schlachter, Uli Wimmel, Harro Modal transition system bounded Petri net synthesis We present a goal-oriented algorithm that can synthesise k-bounded Petri nets (k in N^+) from hyper modal transition systems (hMTS), an extension of labelled transition systems with optional and required behaviour. The algorithm builds a potential reachability graph of a Petri net from scratch, extending it stepwise with required behaviour from the given MTS and over-approximating the result to a new valid reachability graph. Termination occurs if either the MTS yields no additional requirements or the resulting net of the second step shows a conflict with the behaviour allowed by the MTS, making it non-sythesisable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Uli Schlachter and Harro Wimmel 2017 Is Part Of LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2017.6 urn:nbn:de:0030-drops-77802 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.6 eng https://creativecommons.org/licenses/by/3.0/legalcode