Location:
The workshop will take place on gather.town with embedded talks over Zoom. We recommend to join via gather to enjoy the full experience of the workshop, but you can also attend only the talks via Zoom.
Schedule:
17 March morning CET:
- 9:15-9:30 e-coffee on gather.town
- 9:30-10:30 invited talk - Mikołaj Bojańczyk, University of Warsaw - Title: Transducers and their decompositions
- 10:45-11:45 3 short talks:
- 10:45-11:05 Luc Dartois - Title: SD-Regular Transducer Expressions for Aperiodic Transformations
- 11:05-11:25 Sougata Bose - Title: One-way resynchronizability of word transducers
FO transductions, aperiodic deterministic two-way transducers, as well as aperiodic streaming string transducers are all equivalent models for first order definable functions. In this talk, I will present a solution to the long standing open problem of expressions capturing first order definable functions, thereby generalizing the seminal SF=AP (star free expressions = aperiodic languages) result of Schützenberger. Our result also generalizes a lesser known characterization by Schützenberger of aperiodic languages by the so-called SD-regular expressions (SD=AP).
I will show that every first order definable function over finite words captured by an aperiodic deterministic two-way transducer can be described with an SD-regular transducer expression (SDRTE). An SDRTE is a regular expression where Kleene stars are used in a restricted way: they can appear only on aperiodic languages which are prefix codes of bounded synchronization delay (SD).
SDRTEs are constructed from simple functions using the combinators unambiguous sum (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product and the k-chained Kleene-star, where the star is restricted as mentioned.
In order to construct an SDRTE associated with an aperiodic deterministic two-way transducer, (i) we concretize Schützenberger’s SD=AP result, by proving that aperiodic languages are captured by SD-regular expressions which are unambiguous and stabilising; (ii) by structural induction on the unambiguous, stabilising SD-regular expressions describing the domain of the transducer, we construct SDRTEs.This is a joint work with Paul Gastin and Shankara Narayanan Krishna.
The origin semantics of transducers yields several decidability results that are in contrast with classical semantics. In this talk, we consider the one-way resynchronizability problem, which asks whether a given two-way transducer is "close" to a one-way transducer in the origin semantics. We use bounded, regular resynchronizers as a means to compare transducers in the origin semantics and show that it is decidable whether a non-deterministic two-way word transducer can be resynchronized by a bounded, regular resynchronizer into an origin-equivalent one-way transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a non-deterministic two-way transducer is equivalent to some one-way transducer.
- 11:25-11:45 Daniela Petrisan - Title: FunL* -- A generic L*-algorithm for learning automata and transducers
In this talk, I will focus on string-to-string transducers. An important advantage of transducers, as opposed to automata which produce only yes/no outputs, is that transducers can be composed (and therefore also decomposed). I will survey some classes of transducers, ranging from letter-to-letter transducers to polyregular functions, and discuss how they can be decomposed. Some decompositions will be based on the Krohn-Rhodes theorem and its extensions, while others will be in the spirit of λ-calculus with combinators.
In this talk, we present a categorical approach to learning automata over words, in the sense of the L*-algorithm of Angluin. This yields a new generic L*-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a “computation category”. We establish that the sufficient properties for yielding the existence of minimal automata (that were presented in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.
18 March morning CET:
- 9:15-9:30 e- hot beverage
- 9:30-10:30 invited talk - Mohamed Faouzi Atig, Uppsala University - Title: On Solving String Constraints
- 10:50-11:50 3 short talks:
- 10:50-11:10 Rafał Stefański - Title: Single-use transducers for data words
In the talk, I will present versions of two-way and SST transducers for data words, obtained by equipping the register automata (defined by Kaminski & Francez) with appropriate operations. I will also define a single-use restriction and argue that applying it to those models results in many desirable properties. The talk is based on a joint paper with Mikołaj Bojańczyk.
- 11:10-11:30 Jean-Filip Mazowiecki - Title: On polynomial recursive sequences
- 11:30-11:50 Sarah Winter - Title: Continuous Uniformization of Rational Relations and Synthesis of Computable Functions
String data types are present in all conventional programming and scripting languages. In fact, it is almost impossible to reason about the correctness and security of such programs without having a decision procedure for string constraints. A typical string constraint consists of word equations over string variables denoting strings of arbitrary lengths, together with constraints on (i) the length of strings, and (ii) the regular languages to which strings belong. Decidability of this general logic is still open. In this talk, we will discuss recent results on the decidability and decision procedures for string constraints. We will focus on decision procedures that are sound and complete for a well-defined fragment of string constraints. We will also cover a technique that uses a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between these modules allows increasing the precision in an automatic manner.
We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n=n!. Our main result is that the sequence u_n=n^n is not polynomial recursive.
A uniformizer of a binary relation is a function whose graph is contained in the relation and which is defined on the same domain as the relation. It is known that any rational relation of infinite words, i.e. a relation given as a transducer, admits a rational uniformizer. Although rational, those uniformizers are not necessarily well-behaved, in the sense that the ith letter of the output word may depend on the whole infinite input word. In other words, those uniformizers might not be continuous (for the Cantor topology). We address the question of whether rational relations of infinite words can be uniformized by continuous functions. On the negative side, continuous uniformizers might not exist in general and we prove that deciding their existence is algorithmically impossible. On the positive side, we exhibit a large class of rational relations of infinite words, called weakly deterministic rational relations, for which deciding whether a relation in this class admits a continuous uniformizer is an ExpTime-complete problem. This class includes the known classes of deterministic rational relations and automatic relations of infinite words.
As an application of the previous result, and by exploiting a connection between computability and continuity for rational functions of infinite words, we show a result on the synthesis of computable functions from specifications given as weakly deterministic rational relations. In particular, we show that deciding the existence of a computable uniformizer is ExpTime-complete and if there is one, it is possible to effectively synthesize a deterministic two-way transducer computing it. This generalizes the classical setting of Church synthesis to asynchronous implementations which can arbitrarily delay the production of their output signals.
This is joint work with Emmanuel Filiot.