Petri Net Synthesis and Modal Specifications
24. Oktober 2017, 16:00 , 17:30
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
We investigate three problems in this context: Targeted synthesis, minimal over-approximations, and modal
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