Exibard, Léo, Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Département d'Informatique [Bruxelles] (ULB), Faculté des Sciences [Bruxelles] (ULB), Université libre de Bruxelles (ULB)-Université libre de Bruxelles (ULB), Bourse FRIA du F.R.S.-FNRS, Contrat Doctoral Spécifique Normalien de l'ENS Lyon, Aix Marseille Université (AMU), Université libre de Bruxelles (ULB), Pierre-Alain Reynier, Emmanuel Filiot, and EXIBARD, Léo
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 (ℚ, 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 à (ℚ