Strategy synthesis for reactive systems with quantitative objectives

Description

The team of Véronique Bruyère has research activities in the field of formal methods, and more particularly in verification and synthesis of reliable computer systems, by means of algorithmic game theory. During the last years, important progress has been made about reactive systems, that is, systems in continuous interaction with the environment in which they evolve (like controllers embedded in cars or planes). These reactive systems are modelled by graphs the vertices of which model the configurations of the system and the edges of which model the controllable (uncontrollable) actions of the system (environment). The continuous interaction bewteen the system and the environment is modelled by a two-player game played on such a graph, in which the system tries to maintain a coherent behavior against any behavior of the environment. Having a reliable controller for the system amounts to exhibit a winning strategy for the system in this graph game. The existence, construction, implementation and form of such strategies have been studied for different kinds of objectives, first qualitative (like avoiding a deadlock), and more recently quantitative (like minimizing the power consumption). There remain many open questions concerning the combination of qualitative and quantitative objectives.