Synthesis of behavioural controllers for discrete event systems with augmented Petri nets

Speaker

Kai Bollue
Title Synthesis of behavioural controllers for discrete event systems with augmented Petri nets
When 27.05.2008
Where Lecture Room Informatik 11
Abstract Much research has been done on the synthesis of safety controllers for discrete event systems, i.e. controllers which ensure that a given plant stays within feasible parts of the state space by blocking or forcing certain control actions. The goal of the thesis is the much less often regarded synthesis of behavioural controllers, i.e. controllers which actively drive the plant from an initial state (or a set of possible initial states) to a state fulfilling a given set of goal constraints – while still fulfilling an also given set of safety constraints.

Petri nets with certain augmentations have been chosen for the modelling of the uncontrolled plant, due to their ability to display parallel processes and distributes states. Those augmentations include additional arc types, which make the modelling more clear and convenient, as well as mechanisms to model possible interaction with the controller. Transitions are marked as either controllable or uncontrollable, while places are marked as either observable or unobservable, determining the possibilities of the controller to keep track of and influence the operation of the plant. Both safety and goal constraints are assumed to be given by linear constraints on the net marking.

During the synthesis process, the Petri net describing the uncontrolled plant is first transformed into an equivalent set of so called unified transitions, which have linear marking constraints as preconditions for firing and marking changes as firing effect. Based on this set the developed algorithm recursively performs a guided search on the space of possible sequences of control actions (corresponding to firing controllable transitions or querying observable places in the plant model). As indication for how useful a certain control action is in a given state, the firing effect of the corresponding transition with respect to the linear marking constraints is regarded. In each state visited by the algorithm, the reachability graph of the plant model is built, only firing uncontrollable transitions. The leafs of these graphs have to be distinguishable by only regarding observable places. In this case the developed method inserts branchings into the synthesized control algorithm with conditions on the marking of the involved observable places as branching conditions. This means that non-determinism in the plants behaviour can easily be modelled by conflicting transitions.

The resulting control algorithm can be used for several purposes including code generation or synthesis of a Petri net describing the controller for further analysis.