License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2016.15
URN: urn:nbn:de:0030-drops-61603
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6160/
Schlachter, Uli
Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable
Abstract
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.
BibTeX - Entry
@InProceedings{schlachter:LIPIcs:2016:6160,
author = {Uli Schlachter},
title = {{Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {15:1--15:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-017-0},
ISSN = {1868-8969},
year = {2016},
volume = {59},
editor = {Jos{\'e}e Desharnais and Radha Jagadeesan},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6160},
URN = {urn:nbn:de:0030-drops-61603},
doi = {10.4230/LIPIcs.CONCUR.2016.15},
annote = {Keywords: Petri net synthesis, conjunctive nu-Calculus, modal transition systems}
}
|
Keywords: |
|
Petri net synthesis, conjunctive nu-Calculus, modal transition systems |
|
Collection: |
|
27th International Conference on Concurrency Theory (CONCUR 2016) |
|
Issue Date: |
|
2016 |
|
Date of publication: |
|
24.08.2016 |
