07/06/2018 
František Blahoudek
(Masaryk University)
Advances in omegaautomata for Formal Methods
Automata over infinite words (omegaautomata) play
an important role in formal methods. In this talk, I
will present projects that I did during my PhD as well
as some ongoing projects. The presented results range
from studies of impact of automata on explicit model
checking, LTL translations, to generic algorithms on
automata.

06/06/2018 
Marie Van Den Bogaard
(ULB)
Beyond admissibility: Dominance betweens chains of strategies
In this talk, we focus on the concept of rational
behaviour in multiplayer games on finite graphs,
taking the point of view of a player that has access
to the structure of the game but cannot make
assumptions on the preferences of the other
players. In the qualitative setting, admissible
strategies have been shown to fit the rationality
requirements, as they coincide with winning
strategies when these exist, and enjoy the
fundamental property that every strategy is either
admissible or dominated by an admissible
strategy. However, as soon as there are three or
more payoffs, one finds that this fundamental
property does not necessarily hold anymore: one may
observe chains of strategies that are ordered by
dominance and such that no admissible strategy
dominates any of them. Thus, to recover a
satisfactory rationality notion (still based on
dominance), we depart from the single strategy
analysis approach and consider instead chains of
strategies as families of behaviours. We establish a
sufficient criterion for games to enjoy a similar
fundamental property, ie, all chains are below some
maximal chain, and, as an illustration, we present a
class of games where admissibility fails to capture
some intuitively rational behaviours, while our
chainbased analysis does.

09/05/2018 
Guillermo A. Pérez
(ULB)
LearningBased MeanPayoff Optimization in an Unknown MDP under OmegaRegular Constraints
We formalize the problem of maximizing the
meanpayoff value with high probability while
satisfying a parity objective in a Markov decision
process (MDP) with unknown probabilistic transition
function and unknown reward function. Assuming the
support of the unknown transition function and a
lower bound on the minimal transition probability
are known in advance, we show that in MDPs
consisting of a single end component, two
combinations of guarantees on the parity and
meanpayoff objectives can be achieved depending on
how much memory one is willing to use. (i) For all
ε and γ we can construct an onlinelearning
finitememory strategy that almostsurely satisfies
the parity objective and which achieves an
εoptimal mean payoff with probability at least 1 −
γ. (ii) Alternatively, for all ε and γ there exists
an onlinelearning infinitememory strategy that
satisfies the parity objective surely and which
achieves an εoptimal mean payoff with probability
at least 1 − γ. We extend the above results to MDPs
consisting of more than one end component in a
natural way. Finally, we show that the
aforementioned guarantees are tight, i.e. there are
MDPs for which stronger combinations of the
guarantees cannot be ensured.

25/10/2017 
Nathanaël Fijalkow
(Alan Turing Institute of London & University of Warwick)
Parity games algorithms
I will review the current situation on solving parity games.
Recently (2017), three algorithms have been proposed with quasipolynomial running time.
I will describe them and show in a precise sense why there are similar, and discuss how to prove lower bounds.

25/10/2017 
Shibashis Guha
(ULB)
Timed Network Games
Network games are widely used as a model for selfish resourceallocation problems.
In the classical model, each player selects a path connecting her source and target vertex.
The cost of traversing an edge depends on the number of players that traverse it.
Thus, it abstracts the fact that different users may use a resource at different times
and for different durations, which plays an important role in defining the costs of the users in reality.
For example, when transmitting packets in a communication network, routing traffic in a road network,
or processing a task in a production system, actual sharing and congestion of resources crucially depends on time.
We introduce timed network games, which add a time component to network games.
Each vertex v in the network is associated with a cost function,
mapping the load on v to the price that a player pays for staying in v for one time unit with this load.
Each edge in the network is guarded by the time intervals in which is can be traversed,
which forces the players to spend time in the vertices.
We also study the model when the network is equipped with clocks as in timed automata.
Unlike earlier work that add a time component to network games, the time in our model is continuous
and cannot be discretised. In particular, players have uncountably many strategies,
and a game may have uncountably many pure Nash equilibria.
We study properties of timed network games with costsharing or congestion cost functions:
their stability, equilibrium inefficiency, and complexity.
In particular, we show that the answer to the question whether we can restrict attention to integer strategies,
namely ones in which edges are traversed only at integer times, is mixed.

18/10/2017 
Léo Exibard
(ULB)
Twoway Twotape Automata
We consider twoway twotape (alternating) automata accepting pairs of words
and we study some closure properties of this model.
Our main result is that such alternating automata are not closed under
complementation for nonunary alphabets.
This improves a similar result of Kari and Moore for picture languages.
We also show that these deterministic, nondeterministic
and alternating automata are not closed under composition.

21/09/2017 14:00 
Dimitri Watel
(Télécome SudParis)
Synthèse d'une molécule de coût minimum:
complexité, approximabilité et complexité paramétrée.
Un laboratoire ou une entreprise souhaite disposer d'une
molécule et veut pour cela trouver le chemin
réactionnel permettant de la synthétiser.
Il peut premièrement l'acheter à un autre
laboratoire/une autre entreprise.
Il peut également la synthétiser luimême
à partir d'autres molécules.
Pour cela, il doit acheter ou synthétiser ces
molécules et les faire réagir, sachant que
chaque réaction a un coût (économique,
écologique, en ressource humaine, ...).
Une question que l'on se pose est de déterminer
quelles molécules on doit acheter et quelles
réactions on doit effectuer pour synthétiser
la molécule cible avec un coût minimum.
Les personnes souhaitant résoudre ce problème le
font généralement à la main à partir de base
de données répertoriant l'ensemble des
molécules connues et des réactions connues
entre ces molécules.
Nous modélisons ce problème à l'aide d'un
problème de couverture dans un réseau de Petri
représentant un réseau réactionnel.
Dans cette version du problème, l'état initial est
toujours vide, chaque transition est associée à
un coût positif et l'achat d'une molécule est
représenté paré une transition sans
entrée, on cherche à couvrir un état cible,
correspondant aux molécules que l'on souhaite
synthétiser. Nous étudions sa
complexité algorithmique, son approximabilité
polynomiale et sa complexité
paramétrée visàvis de paramètres
naturels du problème.
Nous verrons premièrement que l'on peut démontrer
de forts résultats de difficulté pour ce
problème dû fait de sa proximité avec le problème
de couverture classique: le problème est
EXPSPACEComplet et ne peut être approché avec un
rapport polylogarithmique.
Nous nous intéressons dans une seconde partie à deux variantes
du problèmes, plus proches de l'application pratique.
Une première variante consiste à considérer que le nombre de
transitions que l'on peut effectuer est limité.
Dans la seconde variante, deux exécutions d'une même transition
doivent être consécutives.
La première variante est PSPACEComplète et ne peut être
approchée, mais devient polynomiale si on fixe le
nombre de transitions.
Nous étudions plus en profondeur la complexité
paramétrée du problème
visàvis de ce paramètre.
Le second problème est NPComplet mais ne peut être mieux approchée que la version initiale du problème.
Travail en collaboration avec MarcAntoine Weisser et Dominique Barth

06/09/2017 
Marion Hallet
(UMONS  ULB)
Dynamics and coalitions in sequential games
We consider nplayer nonzero sum games played on finite trees (i.e., sequential games),
in which the players have the right to repeatedly update their respective strategies
(for instance, to improve their payoff wrt to the current strategy profile).
This generates a dynamics in the game which may eventually stabilise to a Nash Equilibrium
(as with Kukushkin’s lazy improvement), and it is thus interesting to study the conditions
that guarantee such a dynamics to terminate.
We build on the works of Leroux and Pauly who have studied extensively the Lazy Improvement Dynamics.
We extend these works by first defining a turnbased dynamics,
proving that it terminates on subgame perfect equilibria,
and showing that several variants do not terminate.
Second, we define a variant of Kukushkin’s lazy improvement where
the players may now form coalitions to change strategies.
We show how properties of the players’s preferences on the outcomes affect
the termination of this dynamics and thereby characterise classes of games
where it always terminates (in particular twoplayer games).
