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.

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.

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:

- to understand these two results and their proofs
- to compare these two classes (is one of them included in the other, is one of the decidable problem reducible to the other?)
- and to look for a larger class of automata with a decidable value 1 problem.

This work can be continued in PhD afterwards.

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:

- Minimal Disclosure in Partially Observable Markov Decision Processes
- and Controllers with Minimal Observation Power

The goals of the internship are:

- understanding the two papers and implementing them as an extension of the tool GAVS+,
- find new algorithms for the synthesis of "frugal" controllers.

This work can be continued in PhD afterwards.