Games for optimal controller synthesis on hybrid automata
Michał Rutkowski · Warwick Research Archive Portal (University of Warwick) · 2011
Hybrid automata are an extension of finite automata obtained by augmenting them with a set of real-valued variables. Hybrid automata are a natural model for hybrid systems, i.e., systems that exhibit both discrete and continuous behaviour. Such systems naturally arise when studying the interaction of a digital controller with an analogue plant. In this thesis we study the problem of optimal controller synthesis for such systems. The goal is to design a control program that will ensure that a system behaves optimally regardless of some uncontrollable external factors. We study this problem from the perspective of two-player games on hybrid automata. In this thesis two variants of hybrid automata are being considered: singleclock timed automata and hybrid automata with strong resets. The first model allows us to capture the passage of time between discrete events, and the other model allows us to capture the more complex dynamics the hybrid systems. The controller synthesis problem is modelled as follows. There are two players: the controller and the adversarial environment. Their interaction is viewed as a multi-stage process, in which the two players interact to create an execution of the hybrid automaton. The problem of synthesising an optimal controller is: given a certain optimisation objective, compute an 'optimal' strategy for the controller player. Executions of the hybrid automaton are assigned two quantities: the price and the reward. Two optimisation objectives are considered: price-per-reward ratio of an infinite execution and the price of reaching a certain state of the hybrid automaton (reachability-price). In this thesis we prove that optimal controllers for the reachability-price objective can be synthesised on single-clock timed automata in EXPTIME. Furthermore, we prove that optimal controllers for reachability-price and average-price-perreward objectives can be synthesised on hybrid automata with strong resets.