Jeux de parité et problème d'accessibilité dans des systèmes à infinité d'états avec paramètres

The most standard model checking approaches are limited to verifying concrete specifications, such as “can we reach a configuration with more than 10 time units elapsing ?”. Nethertheless, for certaincomputer programs, like embedded systems, the constraints depend on the environment. Thus arisesthe need for parametric specifications, such as “can we reach a configuration with more than p timeunits elapsing ?” where p is a parameter which takes values in the non-negative integers.In this thesis, we study parametric pushdown, counter and timed automata and extensions the-reof. In addition to expressing concrete constraints (on the stack, on the counter or on clocks), thesecan employ parametric constraints. The reachability problem for a parametric automaton asks for the existence of an assignment of the parameters such that there exists an accepting run in the underlying concrete automaton. In addition to the reachability problem, we consider parametric parity games, two player games where players alternate chosing assignments for each parameters, then alternate moving a token along the configurations of the concrete automaton resulting from their choice of parameter assignment. We consider the problem of deciding which player has a winning strategy.Parametric timed automata (PTA for short) were introduced in the 90s by Alur, Henzinger andVardi, who showed that the reachability problem for PTA was undecidable, already when only threeclocks can be compared against parameters, and decidable in the case only one clock can. We callsuch clocks that can be compared to parameters parametric clocks. A few years ago, Bundala andOuaknine proved that, for parametric timed automata with two parametric clocks and one parame-ter ((2, 1)-PTA for short), the reachability problem is decidable and also provided a PSPACENEXP lower bound. One of the main results of this thesis states that reachability for (2, 1)-PTA is in factEXPSPACE-complete. For the EXPSPACE lower bound, inspired by previous work by Göller, Haase, Ouaknine, and Worrell, we rely on a serializability characterization of EXPSPACE (in turn originally based on Barrington's Theorem). We provide a programming language and we show it can simulate serializability computations. Relying on a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow, we then show that small (2, 1)-PTA can simulate our programming language. For the EXPSPACE upper bound on (2, 1)-PTA, we first give a careful exponential time reduction towards a variant of parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. We solve the reachability problem for this parametric one-counter automata with one parameter variant, by providing a series of techniques to partition a fictitious run into several carefully chosen subruns. This allows us to prove that it is sufficient to consider a parameter value of exponential magnitude only, which in turn leads to a doubly-exponential upper bound on the value of the only parameter of the (2, 1)-PTA. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in PTA with two parametric clocks and arbitrarily many parameters.Concerning parametric pushdown automata, our main result states that deciding the winner ofa parametric parity game is in (n + 1)-EXP in the case the number of parameters n is fixed, but nonelementary otherwise. We provide the nonelementary lower bound via a reduction of the FO satisfiability problem on words. For the upper bound, we reduce parametric pushdown parity games to higher-order pushdown automata parity games, which are known to be n-EXP complete in the case of stacks of level n.Les approches standard de la vérification de modèle se limitent à des spécifications concrètes, par exemple «est-il possible d'atteindre une configuration après que plus de 10 unités de temps se soient écoulées?». Néanmoins, pour certains types de programmes informatiques, comme les technologies embarquées, les contraintes dépendent de l'environnement. De là émerge la nécessité des spécifications paramétriques, par exemple «est-il possible d'atteindre une configuration après que plus de p unités de temps se soient écoulées?» où p désigne un paramètre dont la valeur reste à spécifier.Dans cette thèse nous étudions des variantes paramétriques de trois modèles classique, les automates à pile, à compteur, et temporisés. En plus d'exprimer des contraintes concrètes (sur la pile, le compteur ou les horloges), ces modèles peuvent exprimer des contraintes paramétriques via des comparaisons avec des paramètres. Le problème de l'accessibilité consiste à demander s'il existe une assignation des paramètres telle que il existe une exécution acceptante dans l'automate concret qui en résulte. En plus de ce problème nous étudions des jeux de parités paramétriques, où deux joueurs choisissent une évaluation pour chaque paramètre chacun leur tour, puis déplacent un jeton dans le graphe de l'automate concret résultant. Nous nous intéressons au problème de décider quel joueur dispose d'une stratégie gagnante.Les automates temporisés paramétriques ont été introduit dans les années 90 par Alur, Henzinger et Vardi, qui ont démontré que le problème de l'accessibilité était indécidable, même avec seulement trois horloges pouvant être comparées à des paramètres, ou horloges paramétriques — mais décidable dans le cas d'une seule horloge paramétrique. Des résultats récents de Bundala et Ouaknine démontrent que dans le cas de deux horloges paramétriques et un paramètre, le problème est décidable ainsi que PSPACE^NEXP-dur. Un des principaux résultats de cette thèse consiste à démontrer le caractère EXPSPACE-complet du problème.La borne inférieure EXPSPACE repose sur des résultats récents du domaine de la complexité avancée. Inspirés par Göller, Haase, Ouaknine, et Worrell, nous visualisons la classe EXPSPACE comme un langage de feuille (vision qui repose sur le théorème de Barrington). Nous introduisons un langage de programmation qui peut reconnaître ce genre de langage de feuille. Nous utilisons ensuite une représentation des entiers sous forme de restes chinois dont Chiu, Davida et Litow ont montré qu'elle permettait de calculer en LOGSPACE la représentation binaire, et démontrons grâce à elle que les automates temporisés paramétriques à deux horloges paramétriques et un paramètre peuvent simuler notre langage de programmation.Pour la borne supérieure, à la façon de Bundala et Ouaknine, nous réduisons le problème au problème de l'accessibilité dans un type particulier d'automates à compteur paramétrique. Par une série de techniques de découpage d'une exécution fictive, nous démontrons que ce problème est dans PSPACE. Étant donné que notre réduction se fait en temps exponentiel, cela conduit à une borne supérieure EXPSPACE pour le problème de l'accessibilité dans les automates temporisés paramétriques à deux horloges et un paramètre.En ce qui concerne les jeux de parités paramétriques pour les automates à piles paramétriques, nous démontrons que le problème de déterminer quel joueur a une stratégie gagnante est dans (n+1)-EXP si le nombre de paramètres est fixé à n, mais nonélémentaire sinon. Le caractère nonélémentaire du problème est démontré par réduction du problème de la satisfaisabilité des formules de la logique du premier ordre. La borne supérieure est obtenue via une réduction aux automates à pile de piles, pour lesquels le problème des jeux de parités est n-EXP-complet dans le cas de n niveaux de piles