PhD Defense
Title

Qualitative Analysis of Synchronizing Probabilistic Systems

When

10th of December, 16h00

The private defense will be on the 24th of November in Brussels. I will also give a talk in LSV (Cachan, France) on the 2nd of December at 11h00.

Where

Université Libre de Bruxelles, Brussels
Campus 'Plaine'
N-O building 5th Floor office NO5.07 (« Solvay » room)
Directions and map at: http://www.ulb.ac.be/campus/plaine/plan-NO.html

Jury

  • Kiefer Stefan: Reviewer
  • Sproston Jeremy: Reviewer
  • Bérard Béatrice: Examiner
  • Filiot Emmanuel: Examiner
  • Katoen Joost-Pieter: Examiner
  • Raskin Jean-François: Examiner
  • Doyen Laurent: Supervisor
  • Massart Thierry: Supervisor

Abstract in english

Markov decision processes (MDPs) are finite-state probabilistic systems with both strategic and random choices, hence well-established to model the interactions between a controller and its randomly responding environment. An MDP can be mathematically viewed as a 1/2-player stochastic game played in rounds when the controller chooses an action, and the environment chooses a successor according to a fixed probability distribution.

There are two incomparable views on the behavior of an MDP, when the strategic choices are fixed. In the traditional view, an MDP is a generator of sequence of states, called the state-outcome; the winning condition of the player is thus expressed as a set of desired sequences of states that are visited during the game, e.g. Borel condition such as reachability. The computational complexity of related decision problems and memory requirement of winning strategies for the state-outcome conditions are well-studied.

Recently, MDPs have been viewed as generators of sequences of probability distributions over states, called the distribution-outcome. We introduce synchronizing conditions defined on distribution-outcomes, which intuitively requires that the probability mass accumulates in some (group of) state(s), possibly in limit. A probability distribution is p-synchronizing if the probability mass is at least p in some state, and a sequence of probability distributions is always, eventually, weakly, or strongly p-synchronizing if respectively all, some, infinitely many, or all but finitely many distributions in the sequence are p-synchronizing. For each synchronizing mode, an MDP can be (i) sure winning if there is a strategy that produces a 1-synchronizing sequence; (ii) almost-sure winning if there is a strategy that produces a sequence that is, for all ε > 0, a (1-ε)-synchronizing sequence; (iii) limit-sure winning if for all ε > 0, there is a strategy that produces a (1-ε)-synchronizing sequence. We consider the problem of deciding whether an MDP is winning, for each synchronizing and winning mode: we establish matching upper and lower complexity bounds of the problems, as well as the memory requirement for optimal winning strategies.

As a further contribution, we study synchronization in probabilistic automata (PAs), that are kind of MDPs where controllers are restricted to use only word-strategies; i.e. no ability to observe the history of the system execution, but the number of choices made so far. The synchronizing languages of a PA is then the set of all synchronizing word-strategies: we establish the computational complexity of the emptiness problems for all synchronizing languages in all winning modes.

We carry over results for synchronizing problems from MDPs and PAs to two-player turn-based games and non-deterministic finite state automata. Along with the main results, we establish new complexity results for alternating finite automata over a one-letter alphabet. In addition, we study different variants of synchronization for timed and weighted automata, as two instances of infinite-state systems.

Abstract in french

Les Markov Decision Process (MDP) sont des systèmes finis probabilistes avec à la fois des choix aléatoires et des stratégiques, et sont ainsi reconnus comme de puissants outils pour modéliser les interactions entre un contrôleur et les réponses aléatoires de l'environment. Mathématiquement, un MDP peut être vu comme un jeu stochastique à un joueur et demi où le contrôleur choisit à chaque tour une action et l'environment répond en choisissant un successeur selon une distribution de probabilités fixée.

Il existe deux représentations incomparables du comportement d'un MDP une fois la stratégie fixée. Dans la représentation classique, un MDP est un générateur de séquences d'états, appelées state-outcome; les conditions gagnantes du joueur sont ainsi exprimées comme des ensembles de séquences désirables d'états qui sont visités pendant le jeu, e.g. les conditions de Borel. La complexité des problèmes de décision et de mémoire requise des stratégies gagnantes pour les conditions dites state-outcome ont été langement étudiées.

Depuis peu, les MDPs sont aussi considérés comme des générateurs de séquences de distributions de probabilités sur les états, appelées distribution-outcome. Nous introduisons des conditions de synchronisation sur les distributions-outcome, qui intuitivement demandent à ce que la masse de probabilité s'accumule dans un (ensemble d') état, potentiellement de façon asymptotique. Une distribution de probabilités est p-synchrone si la masse de probabilité est d'au moins p dans un état; et la séquence de distributions de probabilités est toujours, éventuellement, faiblement, ou fortement p-synchrone si, respectivement toutes, au moins une, une infinité ou toutes sauf un nombre fini de distributions dans la séquence sont p-synchrones. Pour chaque type de synchronisation, un MDP peut être (i) sûrement gagnant si il existe une stratégie qui génère une séquence 1-synchrone; (ii) presque-sûrement gagnant si il existe une stratégie qui génère une séquence (1-ε)-synchrone et cela pour tout ε>0; (iii) asymptotiquement gagnant si pour tout ε>0, il existe une stratégie produisant une séquence (1-ε)-synchrone. Nous considérons le problème consistant à décider si un MDP est gagnant, pour chaque type de synchronisation et chaque mode gagnant: nous établissons les bornes supérieures et inférieures de la complexité de ces problèmes et de la mémoire requise pour une stratégie gagnante optimale.

En outre, nous étudions les problèmes de synchronisation pour les automates probabilistes (PAs) qui sont en fait des instances de MDP où les contrôleurs sont restreints à utiliser uniquement des stratégies-mots; c.à.d. qu'ils ne peuvent pas observer l'historique de l'exécution du système et ne peuvent connaître que le nombre de choix effectués. Les langages synchrones d'un PA sont donc l'ensemble des stratégies-mots synchrones: nous établissons la complexité des problèmes des langages synchrones vides pour chaque mode gagnant. Nous répercutons nos résultats de synchronisation obtenus sur les MDPs et PAs aux jeux à tours à deux joueurs ainsi qu'aux automates finis non-déterministes. Nous établissons de nouveaux résultats de complexité sur les automates finis alternants avec des alphabets à une lettre. Enfin, nous étudions plusieurs variations de synchronisation sur deux instances de systèmes infinis que sont les automates temporisés et pondérés.