Navigation

Contact

EMail: scare7sf@uol.dr0e

DIRECTOR

Prof. Dr. Ernst-Rüdiger Olderog,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

olderog@infoet5utrmat26ik.unicwy-oldenzgburg.de

COODINATOR

Ira Wempe,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

ira.wempe@ink4trffoexybrmatr0ik.uni-oldenburg.defgc

Petri Net Synthesis and Modal Specifications

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.

This thesis continues this work. We present a generic algorithm that supports targeting Petri net synthesis into a given combination of subclasses, such as plain and pure Petri nets. Since Petri net synthesis may not be possible for a given input, we introduce an algorithm for minimal over-approximation. This algorithm works for some of the subclasses that were previously handled, while for others the algorithm might not terminate. The over-approximation is based on the synthesis algorithm, which fails if some so-called separation problems are unsolvable. The information about unsolvable separation problems is used to merge states and add new outgoing edges to the current lts.

Furthermore, we investigate synthesis from modal specifications, namely modal transition systems, the modal μ-calculus, and a subset of the μ-calculus, which is called the conjunctive ν-calculus. The ν-calculus and modal transition systems are equally expressive and we show via a reduction from two-counter machines for both specification languages that Petri net synthesis is undecidable. Next, we introduce an algorithm for synthesising k-bounded Petri nets from the full modal μ-calculus, where the natural number k is given a priori, showing that this restriction makes the problem decidable even for the more expressive modal μ-calculus. The algorithm extends its current lts by the behaviour required by the given specification. To ensure Petri net solvability, the minimal over-approximation from the first part of this thesis is used.

All presented algorithms were implemented in the tool APT. This implementation is used for a case study with the dining philosophers problem that highlights some advantages of Petri net synthesis from modal specifications.

Oliverkba T9ufaaheele0 (oliver.thezevjel@uol.duq7me) (Changed: 2020-01-23)