Synthesis of Switching Controllers for Linear Hybrid Systems

This thesis is focused on the problem of automatically generating switching controllers for the class of Linear Hybrid Game, with respect to safety and reachability objectives. In order to solve the safety control problem, a sound and complete symbolic fix-point procedure on the so-called controllable predecessor operator for safety, called CPreS and based on polyhedral abstractions of the state space, are provided and the termination of each iteration is proved. Some inaccuracies contained in previous characterizations of the problem are identified and solved. In particular, this work shows that the algorithm provided by Wong-Toi [WT97] does not work in some case which are very likely to occur in practice. The error is identified in the heart of this algorithm (the operator flow avoid), and is here fixed by proposing a sound and complete procedure, based on a novel algorithm for computing, within a given location of the automaton, the may reach while avoiding operator RWAm, that is the set of states that may reach a given polyhedral region while avoiding another one. The reachability control problem for hybrid games was never considered in the literature, and the task is not trivially due the fact that, unlike classical results for discrete and real-timed case, the reachability control problem is not dual to the safety control problem. Hence, in order to solve this problem an entirely new study was necessary. This thesis proposed a sound and complete fix-point procedure based on a novel algorithm for computing, within a given location of the automaton, the set of must reach while avoiding operator RWAM, that is the set of states that must reach a given polyhedral region while avoiding another one. The theoretical results of this thesis are then effectively and efficiently implemented on the top of the open source tool PHAVer. The obtained tool, called PHAVer+, is used to present some promising experimental results at the end of this thesis.