Quantitative analysis of stochastic systems : priority games and populations of Markov chains / Bruno Karelović ; sous la direction de Wieslaw Zielonka et de Blaise Genest

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : anglais / English

Catalogue Worldcat

Markov, Processus de

Systèmes stochastiques

Théorie des jeux

Zielonka, Wieslaw (Directeur de thèse / thesis advisor)

Genest, Blaise (1978-....) (Directeur de thèse / thesis advisor)

Asarin, Eugène (Président du jury de soutenance / praeses)

Brihaye, Thomas (19..-....) (Rapporteur de la thèse / thesis reporter)

Haddad, Serge (1956-....) (Rapporteur de la thèse / thesis reporter)

Bouillard, Anne (Membre du jury / opponent)

Gimbert, Hugo (1979-....) (Membre du jury / opponent)

Université Sorbonne Paris Cité (Organisme de soutenance / degree-grantor)

École doctorale Sciences mathématiques de Paris centre (Paris ; 2000-....) (Ecole doctorale associée à la thèse / doctoral school)

Université Paris Diderot - Paris 7 (1970-2019) (Autre partenaire associé à la thèse / thesis associated third party)

Institut de recherche en informatique fondamentale (Paris) (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Cette thèse examine certaines questions quantitatives dans le cadre de deux modèles stochastiques différents. Il est divisé en deux parties : la première partie examine une nouvelle classe de jeux stochastiques avec une fonction de paiement particulière que nous appelons « de priorité ». Cette classe de jeux contient comme sous-classes propre les jeux de parité, largement étudiés en informatique, et les jeux de limsup et liminf, étudiés dans la théorie des jeux. La deuxième partie de la thèse examine certaines questions naturelles mais complexes sur les distributions, étudiées dans le cadre plus simple des chaînes de Markov à espace d'états fini. Dans la première partie, nous examinons les jeux à somme nulle à deux joueurs en se centrant sur la fonction de paiement de priorité. Cette fonction de paiement génère le gain utilisé dans les jeux de parité. Nous considérons à la fois les jeux de priorité stochastiques à tour de rôle et les jeux de priorité simultanés. Notre approche des jeux de priorité est basée sur le concept du point fixe le plus proche (« nearest fixed point ») des applications monotones non expansives et étend l'approche mu-calcul aux jeux de priorité.La deuxième partie de la thèse concerne les questions de population. De manière simplifiée, nous examinons comment une distribution de probabilité sur les états évolue dans le temps. Plus précisément, nous sommes intéressés par des questions comme la suivante : à partir d'une distribution initiale, la population peut-elle atteindre à un moment donné une distribution avec une probabilité dépassant un seuil donné dans l'état visé? Il s'avère que ce type de questions est beaucoup plus difficile à gérer que les questions concernant les trajectoires individuelles : on ne connaît pas, pour le modèle des chaînes de Markov, si les questions de population soient décidables. Nous étudions les restrictions des chaînes de Markov assurant la décision des questions de population.

Résumé / Abstract : This thesis examines some quantitative questions in the framework of two different stochastic models. It is divided into two parts: the first part examines a new class of stochastic games with priority payoff. This class of games contains as proper subclasses the parity games extensively studied in computer science, and limsup and liminf games studied in game theory. The second part of the thesis examines some natural but involved questions about distributions, studied in the simple framework of finite state Markov chain.In the first part, we examine two-player zero-sum games focusing on a particular payoff function that we call the priority payoff. This payoff function generalizes the payoff used in parity games. We consider both turn-based stochastic priority games and concurrent priority games. Our approach to priority games is based on the concept of the nearest fixed point of monotone nonexpansive mappings and extends the mu-calculus approach to priority games.The second part of the thesis deals with population questions. Roughly speaking, we examine how a probability distribution over states evolves in time. More specifically, we are interested in questions like the following one: from an initial distribution, can the population reach at some moment a distribution with a probability mass exceeding a given threshold in state Goal? It turns out that this type of questions is much more difficult to handle than the questions concerning individual trajectories: it is not known for the simple model of Markov chains whether population questions are decidable. We study restrictions of Markov chains ensuring decidability of population questions.