2 Search Results for "Schlachter, Uli"

Document
DOI: 10.4230/LIPIcs.CONCUR.2017.6
k-Bounded Petri Net Synthesis from Modal Transition Systems

Authors: Uli Schlachter and Harro Wimmel

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
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.
Cite as

Uli Schlachter and Harro Wimmel. k-Bounded Petri Net Synthesis from Modal Transition Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{schlachter_et_al:LIPIcs.CONCUR.2017.6,
  author =	{Schlachter, Uli and Wimmel, Harro},
  title =	{{k-Bounded Petri Net Synthesis from Modal Transition Systems}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.6},
  URN =		{urn:nbn:de:0030-drops-77802},
  doi =		{10.4230/LIPIcs.CONCUR.2017.6},
  annote =	{Keywords: Modal transition system, bounded Petri net, synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.15
Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable

Authors: Uli Schlachter

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

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.
Cite as

Uli Schlachter. Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{schlachter:LIPIcs.CONCUR.2016.15,
  author =	{Schlachter, Uli},
  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 =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.15},
  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}
}
  • Refine by Author
  • 2 Schlachter, Uli
  • 1 Wimmel, Harro

  • Refine by Classification

  • Refine by Keyword
  • 1 Modal transition system
  • 1 Petri net synthesis
  • 1 bounded Petri net
  • 1 conjunctive nu-Calculus
  • 1 modal transition systems
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2016
  • 1 2017

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact