A Forward On-The-Fly Approach for Safety and Reachability Controller Synthesis of Timed Systems

ABSTRACT This thesis deals with controller synthesis for real time systems (timed systems). Given a real time system modeled as a Time Petri Net (TPN) with controllable and uncontrollable transitions, the control aims at forcing the system to satisfy properties of interest, by limiting the firing intervals of controllable transitions. We propose, in this thesis, an algorithm to synthesize such controllers for safety / reachability properties. This algorithm, based on the state class graph method, computes on-the-fly the reachable state classes of the TPN while collecting progressively firing subintervals to be avoided so that the property is satisfied. It does not need to compute controllable predecessors and then split state classes until reaching a fixpoint, as it is the case for other approaches based on backward and forward exploration of state space of the system. We prove formally the correctness of the algorithm and show that, in the category of state dependent controllers based on the restriction of firing intervals, the algorithm proposed in this thesis, synthesizes maximally permissive controllers. In order to attenuate the state explosion problem, we show how to combine efficiently this approach with an abstraction by inclusion, convex union or convex hull. Afterwards, we discuss the compatibility of this method with distributed systems and decentralized controllers. Finally, we apply this algorithm to control TPN with controllable and uncontrollable transitions by stopwatch. In this approach, we find the subintervals violating the given properties and our objective is to suspend the tasks (transitions) during their bad subintervals and to resume them later. The controller is synthesized through the same algorithm already introduced. In this approach, we suggest to control time Petri nets by associating stopwatches to controllable transitions and to achieve a controlled time Petri nets.

Résumé

them later. The controller is synthesized through the same algorithm already introduced. In this approach, we suggest to control time Petri nets by associating stopwatches to controllable transitions and to achieve a controlled time Petri nets.