Master internship proposals by Hugo Gimbert

These internships will take place in LaBRI, Bordeaux, under the direction of Hugo Gimbert. An office and a computer will be provided to the intern, as well as the minimal legal internship grant.

Game theory and controller synthesis

Controller synthesis aims at automatically generating hardware devices or programs given a logical specification. A correct controller has to drive the system by means of actions and ensure that the behaviour of the system is correct whatever be the interaction of the system with its environnment. For example, the program controlling an ATM should guarantee that no cash is delivered until the correct pin code has been produced by the current user of the ATM.

Controller synthesis can rely on models and algorithms developped by game theoretists. Various models of interaction have been developped by mathematicians, economists, biologists, computer scientists together with algorithms to analyze and predict the behaviour of rational agents playing these games. Synthesizing a good controller amounts to computing an optimal strategy in a game.

First subject: the value 1 problem for probabilistic automata

Of course in most real-case applications, there is only partial monitoring of the system, and the proper class of games to use are games with imperfect information. For a start, the special case of game with one player and no feedback is interesting. Such games can be seen as probabilistic automata and a basic problem is to decide whether the game has value one or in other words if there exists words accepted with arbitrarily high probability by the automaton.

There has been two recent papers on the subject, see The Decidability Frontier for Probabilistic Automata on Infinite Words by Chatterjee and Tracol and Deciding the Value 1 Problem of Probabilistic Leaktight Automata by Fijalkow, Gimbert and Oualhadj. Each one of these two papers presents a class of automata with a decidable value 1 problem, with very different proofs techniques. The goals of the internship are:

This work can be continued in PhD afterwards.

Second subject: frugal controller synthesis

In practice, systems have huge state space and controllers should be small compared to the system and should work without full monitoring of the system, which is very costly.

This problem has been adressed in two recent papers:

The goals of the internship are:

This work can be continued in PhD afterwards.