Simplifying Transducers using Sequentiality
Simplification de transducteurs en utilisant la séquentialité
Résumé
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) [AC10 ; AC11]. 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 simplification of Finite-State Transducers (FST), a classical problem is the sequentiality problem [Cho77], which asks whether a given FST admits an equivalent sequential one (that is with a deterministic underlying input automaton). For both our results, the proof techniques generalise the framework created around the sequentiality problem.
La synthèse est un domaine de l’informatique consistant à générer des pro- grammes à 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) [AC10 ; AC11]. 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 suffixés par un mot). Ensuite, nous montrons, étant donné un Copyful Concatenation-Free SST, comment décider s’il existe un Concatenation-Free SST équivalent à un seul registre.
Lorsque l’on considère la simplification des Finite-State Transducers (FST), un problème classique est le problème de la séquentialité [Cho77], qui demande si un FST donné admet un FST séquentiel équivalent. Pour nos deux résultats, les techniques de preuves utilisées généralisent le cadre créé autour du problème de séquentialité.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...