2026-07-21T23:17:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6160 2024-03-06T10:38:28Z ddc:004 open_access

Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable Schlachter, Uli Petri net synthesis conjunctive nu-Calculus modal transition systems In this paper, the synthesis of bounded Petri nets from deterministic modal transition systems is shown to be undecidable. The proof is built from three components. First, it is shown that the problem of synthesising bounded Petri nets satisfying a given formula of the conjunctive nu-calculus (a suitable fragment of the mu-calculus) is undecidable. Then, an equivalence between deterministic modal transition systems and a language-based formalism called modal specifications is developed. Finally, the claim follows from a known equivalence between the conjunctive nu-calculus and modal specifications. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Uli Schlachter 2016 Is Part Of LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2016.15 urn:nbn:de:0030-drops-61603 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.15 eng https://creativecommons.org/licenses/by/3.0/legalcode