Cette thèse aborde des sujets liés à la théorie des automates, à la logique et à la théorie des jeux. Ces thèmes sont au cœur de l'informatique théorique depuis de nombreuses décennies. Les travaux de recherche dans ces domaines sont motivés entre autres par des questions de modélisation et de vérification de systèmes. La première partie de la thèse considère les automates finis et la logique temporelle sur des ordres linéaires arbitraires. On y donne une procédure (doublement exponentielle en espace) pour décider la satisfaisabilité d'une formule LTL, utilisant une étape de transformation d'une formule logique en un transducteur synchrone. La seconde partie s'intéresse à des jeux de longueur ordinale. On propose un modèle de jeux à deux joueurs sur des graphes finis, et on montre que la question du vainqueur pour ces jeux peut être résolue en espace polynomial. De plus, on montre qu'il existe des stratégies gagnantes à mémoire finie.

Les jeux à deux joueurs sur des graphes finis ou infinis permettent de modéliser de nombreux problèmes liés à la vérification des systèmes. Le système spécifié dépend de la nature du graphe de jeu considéré tandis que la propriété à vérifier est décrite par la condition de gain. Le premier joueur, Eve, représente un programme qui évolue dans un environnement hostile représenté par le second joueur, Adam. Dans ce formalisme, Eve possède une stratégie gagnante si et seulement si le programme peut être contrôlé de sorte à satisfaire la propriété spécifiée par la condition de gain. On souhaite alors décider si Eve possède une stratégie gagnante et si oui la déterminer, afin de synthétiser ensuite un contrôleur. <br /><br />Dans cette thèse, les graphes de jeu considérés sont des graphes de processus à pile qui offrent une représentation finie simple de systèmes infinis relativement complexes. Sur de tels graphes, on peut considérer des conditions de gain classiques (accessibilité, Büchi ou parité) mais aussi des conditions plus spécifiques au modèle comme celles portant sur le bornage de la pile. On peut également combiner ces dernières entre elles. <br /><br />Une première contribution a été de fournir une représentation des ensembles de positions gagnantes pour les jeux de parité ainsi qu'une nouvelle présentation des résultats connus pour ces derniers. On a alors pu étendre de façon naturelle les techniques de preuves à d'autres conditions de gain, notamment à celles portant sur le bornage de la pile. <br /><br />Une autre contribution a été la description d'une famille de conditions de gain de complexité borélienne arbitraire finie pour lesquelles les jeux (sur des graphes finis ou sur des graphes de processus à pile) restent décidables. <br /><br />L'étude des jeux sur les graphes de BPA et sur les graphes de processus à compteur a permis de proposer des techniques propres à ces modèles qui fournissent alors des bornes de complexité meilleures que celles obtenues dans le cas général des graphes de processus à pile. <br /><br />Enfin, une dernière contribution a été de proposer une solution pour les jeux sur des graphes de processus à pile munis de conditions combinant des conditions régulières et des conditions sur la hauteur de pile et pour des conditions décrites par des automates à pile avec visibilité.