Le problème de la valeur dans les jeux stochastiques

Game theory proved to be very useful in the field of verification of open reactive systems. This is due to the wide variety of games' model that differ in the way players interact and the amount of information players have. In this thesis, we study the value problem for games where players have full knowledge on their current configuration of the game, partial knowledge, and no knowledge. In the case where players have perfect information, we study the value problem for objectives that consist in combination of qualitative and quantitative conditions. In the case of one player stochastic games, we show that the values are computable in polynomial time and show that the optimal strategies exist and can be implemented with finite memory. We also showed that our construction for parity and positive-average Markov decision processes extends to the case of two-player stochastic games. In the case where the players have partial information, we study the value problem for reachability objectives. We show that computing the set of states with value 1 is an undecidable problem and introduce a decidable subclass for the value 1 problem. This sub class is PSPACE-complete in the case of blind controllers and EXPTIME is the setting of games with partial observations.La théorie des jeux est un outils standard quand il s'agit de l'étude des systèmes réactifs. Ceci est une conséquence de la variété des modèles de jeux tant au niveau de l'interaction des joueurs qu'au niveau de l'information que chaque joueur possède. Dans cette thèse, on étudie le problème de la valeur pour des jeux où les joueurs possèdent une information parfaite, information partiel et aucune information. Dans le cas où les joueurs possèdent une information parfaite sur l'état du jeu, on étudie le problème de la valeur pour des jeux dont les objectifs sont des combinaisons booléennes d'objectifs qualitatifs et quantitatifs. Pour les jeux stochastiques à un joueur, on montre que les valeurs sont calculables en temps polynomiale et on montre que les stratégies optimales peuvent être implementées avec une mémoire finie. On montre aussi que notre construction pour la conjonction de parité et de la moyenne positive peut être étendue au cadre des jeux stochastiques à deux joueurs. Dans le cas où les joueurs ont une information partielle, on étudie le problème de la valeur pour la condition d'accessibilité. On montre que le calcul de l'ensemble des états à valeur 1 est un problème indécidable, on introduit une sous classe pour laquelle ce problème est décidable. Le problème de la valeur 1 pour cette sous classe est PSPACE-complet dans le cas de joueur aveugle et dans EXPTIME dans le cas de joueur avec observations partielles