Schlachter, Uli Christian (2018) Petri net synthesis and modal specifications. PhD, Universität Oldenburg.

Preview

Volltext (1176Kb)

Abstract

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.

["eprint_fieldname_title_plus" not defined]

Petrinetz-Synthese und modale Spezifikationen

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Transitionssystem, Petri-Netz, Synthese
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	10 Jan 2019 14:49
Last Modified:	14 Jan 2019 10:34
URI:	https://oops.uni-oldenburg.de/id/eprint/3755
URN:	urn:nbn:de:gbv:715-oops-38362
DOI:
Nutzungslizenz:

Actions (login required)

View Item