Automatic Synthesis of Systems with Data: Synthèse Automatique de Systèmes avec Données
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 t...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Doctoral Thesis |
| Language: | en |
| Published: |
Universite Libre de Bruxelles
2021
|
| Subjects: | |
| Online Access: | https://dipot.ulb.ac.be/dspace/bitstream/2013/333073/5/ContratDiExibard.pdf https://dipot.ulb.ac.be/dspace/bitstream/2013/333073/4/Table_of_Contents.pdf https://dipot.ulb.ac.be/dspace/bitstream/2013/333073/3/Exibard_Automatic_Synthesis_of_Systems_with_Data.pdf http://hdl.handle.net/2013/ULB-DIPOT:oai:dipot.ulb.ac.be:2013/333073 |
| Summary: | 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. === Option Informatique du Doctorat en Sciences === info:eu-repo/semantics/nonPublished |
|---|