[Seminar 29.08.2917] Schlachter
Contact
Director
Prof. Dr. Ernst-Rüdiger Olderog
Coordinator
Ira Wempe
[Seminar 29.08.2917] Schlachter
Uli Schlachter: k-Bounded Petri Net Synthesis from Modal Transition Systems
We present a goal-oriented algorithm that can synthesise k-bounded Petri nets from hyper modal transition systems (hMTS), an extension of labelled transition systems with optional and required behaviour. The algorithm builds a potential reachability graph of a Petri net from scratch, extending it stepwise with required behaviour from the given MTS and over-approximating the result to a new valid reachability graph. Termination occurs if either the MTS yields no additional requirements or the resulting net of the second step shows a conflict with the behaviour allowed by the MTS, making it non-sythesisable.