Transactions on Petri Nets and Other Models of Concurrency XIV 1st ed. 2019 Berlin, Heidelberg : Springer, 2019 (2019), Seite 222-254 1 Online-Ressource (XVII, 255 p. 525 illus., 42 illus. in color)
Application and Theory of Petri Nets and Concurrency Cham : Springer, 2018 (2018), Seite 99-116 Online-Ressource (XI, 427 p. 124 illus, online resource)
Bei der Petrinetz-Synthese soll ein gegebenes endliches beschriftetes Transitionssystem (labelled transition system; LTS) durch ein injektiv beschriftetes Petrinetz gelöst werden, was bedeutet, dass der Erreichbarkeitsgraph des Petrinetzes isomorph zum gegebenen LTS ist. Petrinetz-Synthese fing mit den Arbeiten von Ehrenfeucht und Rozenberg im Jahr 1990 an und wurde seitdem in verschiedene Richtungen erweitert. In dieser Arbeit wird die Synthese von Petrinetz-Teilklassen untersucht, beispielsweise schlichte und schlingenfreie Petrinetze. Unlösbare LTS werden durch Überapproximation behandelt. Als nächstes wird die Synthese von modalen Transitionssystemen (MTS), dem modalem μ-Kalkül und einer Teilmenge des μ-Kalküls, die konjunktiver ν-Kalkül heißt, behandelt. Das Synthese-Problem für MTS und den ν-Kalkül ist unentscheidbar, aber durch eine Einschränkung der betrachteten Petrinetze wird dieses Problem sogar für den ausdruckmächtigeren μ-Kalküls entscheidbar.
In Petri net synthesis, a given finite labelled transition system (lts) should be solved by an injectively labelled Petri net, which means that the reachability graph of the Petri net is isomorphic to the given lts. Petri net synthesis goes back to the work of Ehrenfeucht and Rozenberg in 1990, and has since then been extended in various directions.In this thesis, synthesis for subclasses of Petri nets is investigated, e.g. plain and pure nets. Unsolvable lts are handled by over-approximation. Next, synthesis from modal transition systems (mts), the modal μ-calculus, and a subset of the μ-calculus, which is called the conjunctive ν-calculus, is considered. We show that that the synthesis problem for mts and the ν-calculus is undecidable, but by restricting the Petri nets considered, the synthesis problem becomes decidable even for the more expressive μ-calculus.
Bei der Petrinetz-Synthese soll ein gegebenes endliches beschriftetes Transitionssystem (labelled transition system; LTS) durch ein injektiv beschriftetes Petrinetz gelöst werden, was bedeutet, dass der Erreichbarkeitsgraph des Petrinetzes isomorph zum gegebenen LTS ist. Petrinetz-Synthese fing mit den Arbeiten von Ehrenfeucht und Rozenberg im Jahr 1990 an und wurde seitdem in verschiedene Richtungen erweitert. In dieser Arbeit wird die Synthese von Petrinetz-Teilklassen untersucht, beispielsweise schlichte und schlingenfreie Petrinetze. Unlösbare LTS werden durch Überapproximation behandelt. Als nächstes wird die Synthese von modalen Transitionssystemen (MTS), dem modalem μ-Kalkül und einer Teilmenge des μ-Kalküls, die konjunktiver ν-Kalkül heißt, behandelt. Das Synthese-Problem für MTS und den ν-Kalkül ist unentscheidbar, aber durch eine Einschränkung der betrachteten Petrinetze wird dieses Problem sogar für den ausdruckmächtigeren μ-Kalküls entscheidbar.
In Petri net synthesis, a given finite labelled transition system (lts) should be solved by an injectively labelled Petri net, which means that the reachability graph of the Petri net is isomorphic to the given lts. Petri net synthesis goes back to the work of Ehrenfeucht and Rozenberg in 1990, and has since then been extended in various directions.In this thesis, synthesis for subclasses of Petri nets is investigated, e.g. plain and pure nets. Unsolvable lts are handled by over-approximation. Next, synthesis from modal transition systems (mts), the modal μ-calculus, and a subset of the μ-calculus, which is called the conjunctive ν-calculus, is considered. We show that that the synthesis problem for mts and the ν-calculus is undecidable, but by restricting the Petri nets considered, the synthesis problem becomes decidable even for the more expressive μ-calculus.
CONCUR (28. : 2017 : Berlin) 28th International Conference on Concurrency Theory Saarbrücken/Wadern, Germany : Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 2017 (2017), Artikel Nr. 6, insges. 15 S. 1 Online-Ressource
SOFSEM 2017: Theory and Practice of Computer Science Cham : Springer, 2017 (2017), Seite 163-175 Online-Ressource (XVIII, 526 p. 109 illus, online resource)
