Robust Controller Synthesis in Timed Automata: A Symbolic Approach

Benjamin Monmège
Thursday, 16 May, 2019 - 10:00
Forum B, Campus Plaine

This talk will survey existing and new results on the robust controller synthesis in timed Büchi automata. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. We will first recall how the problem is shown to be PSPACE-complete using game and region-based techniques. The new contribution is a purely symbolic computation using zones only, thus more resilient to state-space explosion problem. The key ingredient is the introduction of branching constraint graphs allowing to decide in polynomial time whether a given lasso is robust, and even compute the largest admissible perturbation if it is. We also make an original use of constraint graphs in this context in order to test the inclusion of timed reachability relations, crucial for the termination criterion of our algorithm. Our techniques are illustrated using a case study on the regulation of a train network.