Ce thème concerne la définissabilité dans divers logiques, souvent avec un aspect calculatoire explicite, que ce soit pour des aspects de décidabilité ou de complexité. Par exemple, le théorème fondateur de Fagin stipule que ESO = NP. Il fait correspondre explicitement définissabilité en logique existentielle du second ordre (ESO) avec la classe des problèmes qu'on peut résoudre en temps polynomial non déterministe (NP).
Les objets d'études sont soit des structures finies (structures relationnelles, classes de graphes finis), avec parfois l'apparition de structures limites infinies; soit des structures infinies directement comme des mots infinis dans un contexte d'arithmétique faible.
On peut ainsi fournir une caractérisation de la définissabilité au premier ordre dans la théorie additive des réels,
qui peut
se re-formuler de manière effective pour une classe très générale de relations, en particulier pour les relations reconnaissables par automate. Une conséquence est la décidabilité de la question de savoir si une relation $n-$aire sur les réels qui est reconnaissable par automate est reconnaissable en toute base.
Un autre sujet typique de complexité descriptive, consiste à mieux appréhender des fragments ou extension de la logique du premier ordre qui sont définis par invariance.
Par exemple,
on peut montrer que sur les classes de degré borné, l'ajout d'un successeur n'apporte pas de pouvoir d'expression à la logique du premier ordre (FO). Cette notion d'invariance correspond au fait qu'en complexité descriptive, typiquement l'entrée d'une machine est ordonnée, alors que le mot d'entrée représente un graphe qui lui ne l'est pas. Ainsi on a un ordre explicite dans le monde calculatoire mais le résultat du calcul doit être indépendant du choix spécifique de cet ordre.
Un ingrédient technique naturel qui apparaît dans ce thème est celui des jeux.
Par exemple,
le problème de synthèse sur les data-words, qui permettent de modéliser des système distribués dont le nombre d'agents est non-borné, revient à décider de l'existence d'une stratégie gagnante dans un jeu à 2 joueur sur des structures potentiellement infinies (voir article à Forte 2024 ci-dessous).
Les jeux sont également un ingrédient important dans le cadre de l'étude systématique de la complexité des problèmes de contraintes quantifiées (QCSP), qu'on peut tous voir comme des problèmes de model-checking de
fragments monotones de FO sur des structures finies fixées qui représentent les contraintes. Ce genre de charactérisation de la complexité s'inscrit dans la continuité des théorèmes de Zhuk et Bulatov qui ont démontré indépendemment la conjecture
de la dichotomie entre P et NP-complet de Feder et Vardi en 2017.
Ainsi, on peut obtenir des résultats de tetrachotomie pour une extension de QCSP avec disjonction et une analyse de la limite entre NP et Pspace-complet pour les QCSP. Dans les deux cas, on peut interpréter les résultats en terme de stratégies et de jeux qui correspondent dans le premier cas à une élimination brutale d'un ou des deux types de quantificateurs et dans l'autre à une limitation très forte de la stratégie du joueur universel.
Julien Grange et Florent Madelaine co-encadrent avec Mamadou Kanté
la thèse de Fatemeh Ghasemi depuis septembre 2023. Cette thèse, à
l'intersection entre logique et graphes, porte sur
la complexité du problème de
model checking (notamment pour la logique étendant FO via
une relation additionnelle de successeur définie par invariance)
ainsi que sur divers questions relatives aux classes de graphes
éparses et aux classes obtenues par transduction de celles-ci.