Soutenance de thèse de Léo EXIBARD

Ecole Doctorale
Mathématiques et Informatique de Marseille
Spécialité
Informatique
établissement
Aix-Marseille Université
Mots Clés
Informatique théorique,Méthodes Formelles,Synthèse Automatique,,
Keywords
Theoretical Computer Science,Formal Methods,Automatic Synthesis,,
Titre de thèse
Synthèse Automatique de Systèmes avec Données
Automatic Synthesis of Systems with Data
Date
Lundi 20 Septembre 2021 à 14:00
Adresse
Faculté des Sciences de Luminy 163 Avenue de Luminy, 13009 Marseille
Inconnue
Jury
Directeur de these M. PIERRE-ALAIN REYNIER Aix-Marseille Université
Rapporteur M. Diego FIGUEIRA Université de Bordeaux
Rapporteur M. Sławomir LASOTA University of Warsaw
Directeur de these M. Emmanuel FILIOT Université Libre de Bruxelles
Examinateur Mme Nathalie BERTRAND INRIA Rennes
Examinateur Mme Orna KUPFERMAN The Hebrew University
Examinateur Mme Karoliina LEHTINEN Aix-Marseille Université
Examinateur M. Jean-François RASKIN Université Libre de Bruxelles

Résumé de la thèse

Les systèmes réactifs sont caractérisés par une interaction constante avec leur environnement : celui-ci fournit un signal d’entrée, auquel le système répond par un signal de sortie, et ainsi de suite à l’infini. L’objectif de la synthèse réactive est de générer automatiquement l’implémentation d’un tel système à partir de la spécification de son comportement. Classiquement, l’ensemble des signaux est supposé fini. Cependant, ce cadre échoue à modéliser des systèmes qui traitent des signaux accompagnés de données issues d’un ensemble potentiellement infini (un identifiant unique, la valeur d’un capteur, etc.), qui doivent être stockées et comparées entre elles. L’objectif de cette thèse est d’étendre la théorie de la synthèse réactive sur les mots à alphabet fini au cas des mots de données. Le domaine de données consiste en un ensemble infini, dont la structure est définie par des prédicats et des constantes, enrichi par un ensemble fini de signaux. Les spécifications et les implémentations sont alors respectivement représentées par des automates et des transducteurs à registres, qu’ils utilisent pour stocker les données. Pour déterminer la transition à prendre, ils comparent la donnée d’entrée au contenu de leurs registres à l’aide des prédicats du domaine. Dans une première partie, nous considérons les problèmes de la synthèse bornée et non-bornée. Dans le premier cas, l’algorithme prend en entrée une borne sur le nombre de registres de l’implémentation, en plus de la spécification à implémenter. Nous considérons plusieurs instances, selon que la spécification est un automate non-déterministe, universel (ou co-non-déterministe), ou encore déterministe, pour plusieurs domaines de données. Tandis que le problème de la synthèse bornée est indécidable pour les spécifications non-déterministes, nous élaborons une approche générique qui permet de le réduire au cas d’un alphabet fini. Celle-ci permet de redémontrer la décidabilité de la synthèse bornée à partir d’automates universels sur (ℕ,=) et d’étendre le résultat à (ℚ,<), y compris en autorisant l’automate à deviner des données, tout cela en 2-ExpTime. Quant à la synthèse non bornée, elle est indécidable pour les spécifications données par des automates non-déterministes ou universels, mais décidable et ExpTime-complète pour les automates déterministes sur (ℕ,=) et (ℚ,<). Nous exhibons également une sous-classe décidable dans le cas de (ℕ,<), à savoir les spécifications unilatérales. Dans une seconde partie, nous examinons comment étendre au cas non-réactif, où l’implémentation est autorisée à attendre d’obtenir plus d’information avant de sélectionner son signal de sortie, toujours dans le cadre des mots de données. Les spécifications sont modélisées par des transducteurs non-déterministes asynchrones, qui produisent un mot (possiblement vide) à chaque fois qu’ils lisent une entrée. Déjà dans le cas fini, un tel problème est indécidable pour cette classe de spécifications. Une manière de contourner la difficulté est de traiter le cas des spécifications fonctionnelles, pour lesquelles chaque suite infinie d’entrées admet au plus une suite de sorties. Pour les implémentations données par des transducteurs déterministes sur l’entrée, le problème est indécidable, aussi nous intéressons-nous au problème de la calculabilité au sens de Turing, classiquement étendue au cas des mots infinis. Nous lions cette notion à celle de continuité pour la distance de Cantor, ce qui nous fournit une caractérisation de la calculabilité qui est décidable pour les fonctions définies par des transducteurs non-déterministes asynchrones sur (ℕ,=) et pour la classe des domaines oligomorphes, qui englobe (ℕ,=) et (ℚ,<). L’étude se conclut par le cas de (ℕ,<), également décidable. Pour ces trois domaines, les problème de calculabilité et ses déclinaisons, ainsi que la fonctionnalité, sont décidables en espace polynomial (PSpace).

Thesis resume

A reactive system is a system that continuously interacts with its environment. The environment provides an input signal, to which the system reacts with an output signal, and so on ad infinitum. In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. In the classical setting, the set of signals is assumed to be finite. However, this assumption is not realistic to model systems which process sequences of signals accompanied with data from a possibly infinite set (e.g. a client id, a sensor value, etc.), which need to be stored in memory and compared against each other. The goal of this thesis is to lift the theory of reactive system synthesis over words on a finite alphabet to data words. The data domain consists in an infinite set whose structure is given by predicates and constants enriched with labels from a finite alphabet. In this context, specifications and implementations are respectively given as automata and transducers extended with a finite set of registers that they use to store data values. To determine the transition to take, they compare the input data with the content of the registers using the predicates of the domain. In a first part, we consider both the bounded and unbounded synthesis problem; the former additionally asks for a bound on the number of registers of the implementation, along with the specification. We do so for different instances, depending on whether the specification is a nondeterministic, universal (a.k.a. co-non-deterministic) or deterministic automaton, for various domains. While the bounded synthesis problem is undecidable for non-deterministic specifications, we provide a generic approach consisting in a reduction to the finite alphabet case, that is done through automata-theoretic constructions. This allows to reprove decidability of bounded synthesis for universal specifications over (ℕ,=), and to obtain new ones, such as the case of a dense order, or the ability of data guessing, all with a 2-ExpTime complexity. We then move to the unbounded synthesis problem, which is undecidable for specifications given by non-deterministic and universal automata, but decidable and ExpTime-complete for deterministic ones over (ℕ,=) and (ℚ,<). We also exhibit a decidable subclass in the case of (ℕ,<), namely one-sided specifications. In a second part, we lift the reactivity assumption, considering the richer class of implementations that are allowed to wait for additional input before reacting, again over data words. Specifications are modelled as non-deterministic asynchronous transducers, that output a (possibly empty) word when they read an input data. Already in the finite alphabet case, their synthesis problem is undecidable. A way to circumvent the difficulty is to focus on functional specifications, for which any input sequence admits at most one acceptable output. Targeting programs computed by input-deterministic transducers is again undecidable, so we shift the focus to deciding whether a specification is computable, in the sense of the classical extension of Turing-computability to infinite inputs. We relate this notion with that of continuity for the Cantor distance, which yields a decidable characterisation of computability for functional specifications given by asynchronous register transducers over (ℕ,=) and for the superseding class of oligomorphic data domains, that also encompasses $(ℚ,<)$. The study concludes with the case of $(ℕ,<)$, that is again decidable. Overall, we get PSpace-completeness for the problems of deciding computability and refined notions, as well as functionality.