Trends in Transformations

Speakers

Title : First Order and Regular List Functions

Abstract : In this talk, I will present a characterisation of FO and MSO-transduction with a flavour of functional programming. Indeed, I will define classes of functions, called list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting them together using four combinators (most importantly, composition of functions). Our main results are that first-order list functions are exactly the same as FO-transductions, under a suitable encoding of the inputs; and the regular list functions are exactly the same as MSO-transductions. This is a joint work with Mikolaj Bojanczyk and Krishna S.

Tutorial : Specification and Computation of Word Transductions

Abstract : A finite word transduction is a binary relation of finite words. This talk surveys important old and recent results of the literature about automata models for computing transductions (aka transducers), as well as their main associated decision problems (functionality, equivalence). Then, results extending Büchi's Theorem to well-behaved classes of transductions are presented. In particular, logical formalisms to express transductions and correspondences with transducer models are exposed in this talk. The talk is concluded by briefly presenting other recent results from the literature.

Second Talk : Logics for Transductions and Transducers

Abstract : This talks exposes recent results on two different logics for two different purposes. The first logic is a logic specifically tailored to express binary word relations, aka transductions. In this logic, transductions are seen as sets of bipartite graphs, composed of the input word (with a linear-order on its positions), the output word (with a linear order on its positions) and some mapping, called the origin mapping, relating output to input positions. We show that this logic is very expressive, subsuming MSO-transductions à la Courcelle and Engelfriet, but still retains interesting decidability properties. This is a joint work with Nathan Lhote and Luc Dartois published at LICS'18. The second logic is a "meta" logic which is well-suited to express structural properties of finite state transducers, or finite state automata equipped with some output mechanism in general. Our goal was to provide a useful logic to express as simply as possible structural patterns which are for instance used to characterise finite ambiguity, sequentiality, or exponential ambiguity. We show, in the case of finite automata, sum-automata and transducers, that model-checking a fixed formula of this logic against an automata of the latter kinds, can be done in NLogSpace. This entails for instance that ambiguity of finite automata, or sequentiality of transducers, is decidable in NLogSpace, hence polynomial time. This latter work is joint with Nicolas Mazzocchi and Jean-François Raskin. It was published in DLT'18.

Title : Origin semantics and equivalence problem for non-functional transducers

Abstract : While functional transducers enjoy decidable equivalence, this becomes false when we consider non-functional transducers. In 2014, Bojańczyk introduced the so-called origin semantics of transducers, which informally amounts to have every letter of the output word remember what letter of the input word was processed when it was produced. In this new semantics, the equivalence relation is finer than in the classical semantics (e.g. unary reverse and unary identity are separated). The goal of this talk is to show that the origin equivalence problem is decidable for the main non-functional transducers classes (streaming string transducers and two-way). The two-way case being presented in FSTTCS'18, we will focus on the streaming string transducer (SST) case, and give an exact characterisation of the origin semantics of SSTs, when seen as a set of graphs. We will also wonder if this origin semantics is not too restrictive, namely, it would be desirable to detect that two transducers produce the same relation, but one has some small delay in its productions compared to the other. We will introduce a notion of resynchronisers which modifies the origin mapping of a relation, and show that it is actually possible to retain equivalence modulo a resynchroniser of a particular class. We leave for now open if that notion includes the resynchronisers of Filliot et al. in the one way case. This talk is based on joint work with Mikołaj Bojańczyk, Laure Daviaud and Bruno Guillon (ICALP'17), and Sougata Bose, Anca Muscholl and Gabriele Puppis (FSTTCS'18).

Algebraic and logical characterizations of rational transductions

Abstract : Rational word languages can be defined by several equivalent means: finite state automata, rational expressions, finite congruences, or monadic second-order (MSO) logic. The robust subclass of aperiodic languages is defined by: counter-free automata, star-free expressions, aperiodic (finite) congruences, or first-order (FO) logic. In particular, their algebraic characterization by aperiodic congruences allows to decide whether a regular language is aperiodic. We lift this decidability result to rational transductions, i.e. word-to-word functions defined by finite state transducers. In this context, logical and algebraic characterizations have also been proposed. Our main result is that one can decide if a rational transduction (given as a transducer) is in a given decidable congruence class. As a consequence, it is decidable if a rational transduction is aperiodic, and we show that this problem is PSPACE-complete. This talk is based on works with Emmanuel Filiot, Olivier Gauwin and Anca Muscholl: LICS2016, FSTTCS2016, FSTTCS2018, to appear in LMCS.