thesis

Simplifying transducers using sequentiality

Defense date:

Nov. 26, 2019

Edit

Institution:

Aix-Marseille

Disciplines:

Abstract EN:

Synthesis is a field of computer science that consists in generating programs from abstract specifications. Specifications are often described via a logical formalism and programs are obtained as models of transformation. While, in the specifications, it is useful to express properties of the desired programs using some forms of non-determinism, we usually want to avoid it in the outcome of synthesis, for obvious efficiency reasons. Generally speaking, this leads us to the need to simplify the synthesised transformation models, in order to optimise their evaluation or translation into practical applications.In this thesis, the transformation models we are interested in are expressed as Streaming String Transducers (SST) [AČ10 ; AČ11]. An SST is a deterministic finite-state automaton equipped with a finite count of registers that can be used to construct an output word. These registers can be updated by using register concatenation or by prepending or appending finite words. We are interested in the challenging problem of register minimisation, which consists, given an SST, in computing an equivalent SST with a minimal number of registers. As a first step to support this general model, we constrain how the registers can be operated on: namely, the registers cannot be concatenated one to another.We present two main contributions. First, we devise a procedure allowing to minimise registers in the class of copyless appending SSTs (in this class, registers can only be appended to). Second, we show, given a copyful concatenation-free SST, how to decide whether there exists an equivalent concatenation-free SST with a single register.When considering the [...]

Abstract FR:

La synthèse est un domaine de l'informatique consistant à générer des programmes à partir de spécifications abstraites. Les spécifications sont souvent décrites à l'aide d'un formalisme logique et les programmes sont obtenus sous la forme de modèles de transformation. Alors qu'il est utile de pouvoir exprimer les propriétés des spécifications avec du non-déterminisme, nous souhaitons en général obtenir des modèles déterministes pour des raisons évidentes d'efficacité. Ceci nous amène à vouloir simplifier les modèles synthétisés afin d'optimiser leur évaluation ou leur représentation concrète dans un programme.Dans cette thèse, les modèles de transformations qui nous intéressent sont exprimés par des Streaming String Transducers (SSTs) [AČ10 ; AČ11]. Un SST est un automate fini déterministe équipé d'un nombre fini de registres qui peuvent être utilisés pour élaborer un mot de sortie. Ces registres peuvent être mis à jour en utilisant la concatenation de registres ou en les préfixant ou suffixant par des mots finis. Nous sommes intéressés par le problème ambitieux de la minimisation de registres, qui consiste, étant donné un SST, à calculer un SST équivalent avec un nombre minimal de registres. Comme première étape à la prise en compte de ce modèle très expressif, nous contraignons la manière dont les registres sont manipulés: ils ne peuvent pas être concaténés les uns aux autres (cette classe est appelée Concatenation-Free SST).Nous présentons deux contributions principales. Tout d'abord, nous élaborons une procédure permettant de minimiser le nombre de registres dans la classe des Copyless Appending SSTs (dans cette classe, les registres ne peuvent qu'être [...]