Algebra and Combinatorics of Parity Games
Algebre et Combinatoire des Jeux de Parité
Résumé
Parity games are the combinatorial description of the theory of binary infimums, and supremums, and of the least and greatest fixed points over complete lattices. Roughly speaking, the parity games formalism may be understood as a μ-calculus over complete lattices. Hierarchies and logical expressiveness are at the core of fixed-point theory. The first part of this the- sis is devoted to consider the variable hierarchy problem within the lattice μ-calculus. Earlier works on this problem within the propositional modal μ- calculus have derived a complexity measure, the so called entanglement. The latter is the combinatorial counterpart of the variable hierarchy. The second part of this thesis is devoted to consider the entanglement as a pure graph theoretic measure, independently of its origins in fixed-point theory. Further results will be proved in this direction, such that the recognization of graphs of bounded entanglement, the tree decomposition of these graphs, and the closure under minors.
Les jeux de parité sont la représentation combinatoire de la théorie des infimums, suprimums, et du plus petit point fixe et du plus grand point fixe sur les treillis complets. En gros, le formalisme des jeux de parité peut être considéré comme un $\mu$-calcul sur les treillis complets. Les hiérarchies et le pouvoir expressif sont un thème centrale dans la théorie des points fixes. La première partie de cette thèse est consacrée à l'étude du problème de la hiérarchie des variables sur le $\mu$-calcul des treillis. Des travaux antérieurs sur ce problème dans le cas du $\mu$-calcul propositionnel modal ont dégagé une mesure de complexité des graphes: c'est \emph{l'enchevêtrement}. Le dernier est la partie combinatoire de la hiérarchie des variables. La deuxième partie de cette thèse est consacrée à l'étude de l'enchevêtrement dans le contexte de la théorie des graphes, indépendamment de son origine dans la théorie des points fixes. Plusieurs résultats seront démontrés dans cette direction, tels que la reconnaissance des graphes d'enchevêtrement borné, la décomposition arborescente de tels graphes, et la fermeture par mineurs.
Loading...