In this talk, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS), a method known to be scalable to large state spaces. We will present their theoretical guarantees. Formal analysis of MCTS is notably challenging, and we will discuss recent results in that area. Moreover, we augment the MCTS algorithm with a notion of symbolic advice, and show that its theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We illustrate our techniques using a scheduling problem and the popular game Pac-Man.

Cooperative rational synthesis is the problem of computing a Nash equilibrium that satisfies the objective of a designated player, the “controller”. In this paper, we tackle this problem in the presence of several resources, where each action may increase or decrease some of the resources. We investigate the problem of synthesizing the controller strategy such that there exists an individually rational behavior of all the agents that satisfies the controller’s objective and does not deplete any of the resources.

We consider two types of agents: careless and careful. Careless agents only care for their temporal objective, while careful agents also pay attention not to deplete the system’s resource. We show that the problem is undecidable with at least two resources, and decidable for either a single resource or in the presence of a fixed upper bound on all the resources, and study the complexity for the decidable cases.

Controlling the Access of Data in Database management systems is a classical problem and it has been solved through different mechanisms. One of the most common implemented in most Databases management systems is the mechanism of views, i.e defining the accessible data of a user as the result of a query. This mechanism is also used in principle in other systems such as in social networks.

Unfortunately, this approach has some defaults. Even though it does not leak any secret information, the user seeing the data can infer some of these secret data by using different knowledge such as the logical definition of the query used to define the accessible data and different property of the database.

In this talk, I will present a formalism allowing to check when a set of views do not leak any information even through this kind of attacks.