About Trends

The beautiful and robust theory of regular languages is based on four fundamental pillars : expressions, automata, logic and algebra. The class of languages denoted by regular expressions corresponds to the class of languages recognized by finite state automata, to the class of languages definable in monadic second order logic (MSO) with one successor, and to the class of languages whose syntactic monoid is finite. Extensions of the pillars of language theory to transformations (functions or relations) from words has been an active area of research recently. The aim of this workshop is to bring together researchers and students interested in theory and applications of formal models of transformations (transducers). Simply put, a transducer is an automaton extended with outputs. The workshop begins with a tutorial talk by Emmanuel Filiot, telling us of the state of the art in transducers, and will be followed by specific technical talks on recent trends in transducers.


Speakers

  • Laure Daviaud, University of Warwick
  • 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.

  • Emmanuel Filiot, ULB
  • 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.

  • Vincent Penelle, LaBRI
  • Title : Origin semantics and equivalence problem for non-deterministic transducers

    Abstract : Coming Up

  • Nathan Lhote, University of Warsaw
  • 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.

    Event Schedule (Apart from the tutorial, the order of the remaining talks are subject to change)

    Schedule

    08:30-09:20 Registration
    09:20-09:30 Opening Remarks
    09:30-10.30 Tutorial by Emmanuel Filiot
    10:30-11:00 Tea Break
    11:00-12:00 Laure Daviaud
    12:00-13:00 Vincent Penelle
    13:00-14:00 Lunch
    14:00-15:00 Nathan Lhote
    15:00-15:30 Tea Break
    15:30-16:30 Emmanuel Filiot






    Venue

    SEAS,
    Ahmedabad University,
    Ahmedabad,
    Gujarat