Theory and Applications of Transducers

The focus of my research is to develop foundations of formal models to express string-to-string transformations — such as streaming string transducers and transducer expressions — and to investigate their applications in formal analysis and verification of systems. The rich theory behind regular and omega-regular languages is the cornerstone of the automatic verification technology (model-checking) of reactive systems. For instance, the interplay between expressive formalisms to define regular languages — such as (non-) deterministic finite automata, regular expressions, monadic second order logic — has resulted in modeling and specification formalisms that can be efficiently and automatically verified. While regular languages can only express properties of acceptable program traces, regular transformations can provide the vocabulary to express relations between input traces and observations sequences. Efficient decision procedures for such transformations can then be used in modular verification of safety and security properties of programs expressed as compositions of transducers.

The contributions of our current research to the landscape of regular transformations are summarized below.

• A very fundamental result in the theory of transductions is the equivalence of MSO transductions and two-way transducers. This result is one of the corner stones in theoretical computer science, since it extends the classical result of Buchi-Elgot-Trakhtenbrot which shows the equivalence of MSO and regular languages, to the level of transductions. A subcase of this theorem is obtained when one restricts the input language to counter-free languages. One then obtains an equivalence with First Order Logic. This result works on both finite as well as infinite words. A natural question to ask is whether there is a counterpart when one looks at transformations. To be precise, do Courcelle's FO transformations coincide with a particular subclass of SSTs and 2WST? And, is this result robust for finite and infinite words. In our paper published in fsttcs’16, we answer this question in the affirmative for the infinite words case, thereby showing that FO transformations coincide with aperiodic SSTs (a subclass of SSTs) and aperiodic two way transducer with star-free look-ahead.

• There exists a compact and very useful representation of regular languages in form of regular expressions (also known as regex in programming). We have recently extended this result in case of transformations and we call it regular transducer expression(RTE). We have shown equivalence of RTE and omega-RTE with regular and omega-regular transformations respectively. All results can be found in this paper published in LICS’18.

Computability of Transducer definable function: The class of regular functions from infinite words to infinite words is characterised by MSO-transducers, streaming omega-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. This paper proposes a decision procedure for the following question : given a regular function f, is f computable (by a Turing machine with infinite input)? For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability.