Cette thèse s'inscrit dans le contexte du calcul en temps infini. Par cette désignation, nous faisons référence au temps indicé par des ordinaux, ces derniers possédant de bonnes propriétés pour ``compter''en leur long. En 2000, le modèle des machines de Turing à temps infini fut proposé par Hamkins et Lewis. Ce modèle généralise le processus de calcul des machines de Turing aux étapes de temps représentées par des ordinaux. Dans ce modèle de calcul, les étapes sont indicées par des ordinaux dénombrables, bien que le ruban soit toujours indicé par des entiers naturels. Les entrées du modèle sont donc les suites infinies de lettres. Un certain nombre de comportements nouveaux et étonnants apparaissent avec ces machines. Dans notre thèse, nous nous intéressons à certains de ces comportements.Naturellement, plus les temps de calcul sont longs, plus le modèle est puissant, et plus il devient possible de décider de nouveaux ensembles.À partir d’ordinaux assez grands, de nouvelles propriétés structurelles apparaissent également. L'une d'entre elles est l'existence de brèches dans les temps possibles d'arrêts de programmes. Lorsque ces brèches furent découvertes, de premiers liens entre elles et le caractère admissible des ordinaux qui les commencent furent établis. Notre approche utilise l'algorithmique pour préciser les liens entre les propriétés logiques des ordinaux et les propriétés calculatoires de ces machines à temps infini.Plus précisément, grâce à des des algorithmes spécifiques, nous découvrons et prouvons de nouvelles propriétés sur ces brèches,amenant à une meilleure compréhension de leur structure. Nous montrons notamment que les brèches peuvent être de toutes les tailles (limites) écrivables, qu'il en existe même de taille au moins aussi grande que leur ordinal de début. Jusqu’à la première brèche ayant cette caractéristique, la structure des brèches est assez proche de celle des ordinaux : elles apparaissent en ordre croissant en fonction de leur taille. Nous montrons également que jusqu'à cette brèche spéciale, si les ordinaux admissibles sont exactement les ordinaux débutant les brèches, au-dessus, des ordinaux admissibles peuvent apparaître au milieu de très grandes brèches et la structure des brèches devient désordonnée. / This thesis is centred on the study of infinite time computations. Infinite time here means having a time axis indexed by ordinals — the ordinals are convenient objects along which we can count. The infinite time Turing machine model was introduced by Hamkins and Lewis in 2000. This model generalises the Turing machine computation model to ordinal time. In this model, stages are indexed by (countable) ordinals, even though the tape is indexed by the integers as in the classical model. This model can thus now have infinite strings as input. The main focus of this thesis is the study of some of the new and surprising behaviours that these machines exhibit. Naturally, the longer, i.e., the greater ordinal, the computations run, the more powerful the model is, i.e. it computes/recognizes more sets. If the computations run beyond certain ordinal times, new structural properties also appear. One of these properties is the existence of gaps in the halting times of the machines. When these gaps had been discovered, some first links had been established between these gaps and the admissible character of the ordinals starting them. Our approach uses algorithmics as a mean to emphasize the links between the logical properties of the ordinals involved and the computational properties of the infinite time Turing machines. Moreover, thanks to some specific algorithms, we discover and prove new properties of these gaps, leading to a better understanding of their structure. We show in particular that gaps can have precisely every possible writable ordinal size and that there are gaps whose length is greater or equal than their starting ordinal point. Until the first of such a gap, the gaps appear in increasing sizes. We also show that even if, before this special gap, admissible ordinals only appear at the beginning of gaps, the gaps structure becomes quite disordered beyond that point, with admissible ordinals appearing not only at the beginning but also inside some (huge) gaps.

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.