Petri Net Synthesis and Modal Specifications

24. Oktober 2017, 16:00 , 17:30

Veranstalter:  Uli Schlachter, Universität Oldenburg
Ort:  OFFIS, Escherweg 2, Raum D21

Abstract:

Given a specification describing some behaviour, algorithms for Petri net synthesis try to find a Petri net

with this behaviour. For example, a specification can be a regular language and a Petri net is wanted in

which only words from this language can fire. This allows to go from a sequential specification, like a finite

automaton describing a regular language, to a concurrent system, a Petri net. Existing approaches for Petri

net synthesis not only solve languages up to language-equivalence, but also labelled transition systems up

to isomorphism.

We investigate three problems in this context: Targeted synthesis, minimal over-approximations, and modal

specifications.

In targeted synthesis, not just any Petri net is wanted, but a class of Petri nets is targeted. Such a class can

be plain Petri nets, which means that arcs can have at most weight one. Based on an existing algorithm for

Petri net synthesis, we identified a number of such classes that can be incorporated into the algorithm.

Minimal over-approximation deals with unsolvable specifications. Instead of returning a failure, the specifi-

cation is amended so that some extra behaviour is allowed. This is not only possible for Petri nets in gen-

eral, but also for some classes of nets.

While traditional specification only require some behaviour to be present, modal specifications also allow

to express some optional behaviour. We investigate two kinds of modal specifications, Modal Transition

Systems (Larsen, 1989) and the modal μ-calculus (Kozen, 1983). For both kinds, synthesis is undecidable

in general. Thus, we target k-bounded Petri nets where the value k is another input to the algorithm. In such

nets no place may ever contain more than k tokens. With this restriction, the synthesis problem becomes

decidable and we present a novel algorithm for it. This algorithm uses the minimal over-approximation

mentioned previously and also supports some classes of nets.

Betreuer: Prof. Dr. Eike Best