# DELTA: DÉfis pour la Logique, les Transducteurs et les Automates

DELTA is an **ANR project** involving the groups **CRISTaL**, **LaBRI**, **IRIF** and **LIF**. that started in 2017. The **official page** is in LaBRI. The **project leader** is Marc Zeitoun.

Members are P. Bourhis, F. Baschenis, O. Carton, Th. Colcombet, D. Gallois, Diego Figueira, O. Gauwin, N. Lhote, B. Monmege,A. Muscholl, T. Pierron, J.-É. Pin, T. Place, G. Puppis, F. Reiter, P.A. Reynier, J.M. Talbot, D. Villevalois, P. Weil and M. Zeitoun,

—

## DELTA Meeting in Paris: 26-28 March 2018

This is a three full days meeting to be held in **amphithéâtre Turing** from March 26 to 28.
Details to come.

### Monday 26 March

9h00-10h00 Accueil (café + viennoiseries)

10h00-10h30 **Nathanaël Fijalkow** *Learning with a bad teacher*
slides

10h45-11h15 **Peter Habermehl** *(Regular) transformation of data words*
slides

Joint work with Antoine Durand-Gasselin

11h30-12h15 **Vincent Penelle** *Which classes of origin graphs are generated by transducers?*
slides

*regular word transductions*, which form a robust class of (partial) functions from (finite) words to (finite) words. Regular transduction are for instance recognized by deterministic 2-way finite automata with outputs or deterministic streaming string transducers. We start from the observation that the various equivalent models of

*transducers*capturing the class, actually provide more than a function from words to words. Indeed, one can also reconstruct

*origin information*which says how positions of the

*output*word originate from positions of the

*input*word. With this semantics,

*transductions*are viewed as sets of particular graphs, called

*origin graphs*. This allows us to express properties, such as

*«the output is a permutation of the input»*or

*«the transduction is a right-to-left one-way transduction»*, using MSO Logic.

After an introduction presenting the general framework, I will briefly show that MSO Logic is decidable on the *origin semantics* of regular transducers, yielding procedures to check formulas such as given above.
Then, I will characterize the families of origin graphs which corresponds to the semantics of streaming string transducers.

This is joint work with Mikolaj Bojanczyk, Laure Daviaud and Bruno Guillon, and has been published to ICALP17.

—

12h30-14h00 Repas au restaurant Buffon (pour les orateurs et les membres de Delta)

—

14h00-14h45 **Sougata Bose** *On resynchronization of transducers with origin*
slides

We also introduce a notion of logical resynchronization which allows us to transform the origins in the origin semantics. We then consider a variant of the equivalence problem modulo logical resynchronizations. This extends the work of Filiot et al who considered equivalence in origin semantics and resynchronizers for one-way transducers.

This is ongoing joint work with Anca Muscholl, Gabriele Puppis and Vincent Penelle.

15h00-15h30 **Maria Emilia Descotte** *Resynchronizing Classes of Word Relations*
slides

15h30-16h00 Pause café

16h00-16h45 **Luc Dartois** *A logic for transduction with regular synthesis*
slides

In LT, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. LT is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, LT has decidable satisfiability problems. The main contribution is a synthesis result: it is always possible to synthesis a regular function which satisfies the specification.

Finally, I explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.

### Tuesday 27 March

9h00-9h30 Accueil (café + viennoiseries)

9h30-10h00 **Pierre Alain-Reynier** *Copyful Streaming String Transducers*
slides

On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this work, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of deterministic copyful SST. Our contributions are as follows: (i) HDT0L systems and total deterministic copyful SST have the same expressive power, (ii) the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in linear time. As a consequence, equivalence of deterministic SST is decidable, (iii) the functionality of non-deterministic copyful SST is decidable, (iv) determining whether a deterministic copyful SST can be transformed into an equivalent deterministic copyless SST is decidable in polynomial time.

10h15-10h45 **Jean-Marc Talbot** *Two-Way Parikh Automata with a Visibly Pushdown Stack*
slides

10h45-11h15 Pause café

11h15-12h15 (Guest lecture) **Guillaume Lagarde** et **Sylvain Périfel** *a “one-bit catastrophe” but not a tragedy*
slides

—

12h30-14h00 Repas au restaurant Buffon (pour les orateurs et les membres de Delta)

—

14h00-14h45 **Jean-Éric Pin** *Regularity preserving transductions*
slides

**regularity preserving**if the inverse image of a regular language under this function is again regular. The description of regularity-preserving functions is a long-term objective, but in spite of intensive research, it is still out of reach. I will present a topological characterisation of these functions and I will give numerous examples and problems on them.

More generally, if C is a class of languages, a function (or more generally a transduction) is said to be **C-preserving** if the inverse image of a language in C under this function is again
in C. Time permitting, I will present some recent results on this topic.

15h00-15h45 **Adrien Boiret** *Using Hilbert methods to decide equivalence of transducers*
slides

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

- We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.
- We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

16h00-16h30 Pause café

16h30-17h00 **Laure Daviaud** *When is containment decidable for probabilistic automata?*
slides

This is a joint work with Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez and James Worrell.

17h15-19h15 Réunion des responsables du projet ANR Delta

—

19h30-21h30 Restaurant

—

### Wednesday 28 March

9h00-9h30 Accueil (café + viennoiseries)

9h30-10h15 **Marc Zeitoun** *Separating without any ambiguity*
slides

This talk presents old and new results regarding a standard operator on classes of languages: unambiguous polynomial closure. We show that if C is a class of regular languages having some mild properties, then the membership problem for its unambiguous polynomial closure UPol(C) reduces to the same problem for C. I will sketch a new, self-contained and elementary proof of this result. A corollary is that unambiguous polynomial closure coincides with alternating left and right deterministic closure. Finally, I will present separation results in the case when C is a finite class.

10h30-11h0 **Varun Ramanathan** *On the separation and covering problems when a logical signature is enriched with modulo predicates*
slides

Monadic second order logic (MSO[<]) and first order logic (FO[<]) with order predicates provide an important logical framework to study different classes of regular languages. We consider the class of modular predicates (MOD), with which we can specify positions in a finite word modulo some fixed integer d. Enriching FO and its fragments with modular predicates strictly increases their power, while staying in the realm of MSO[<] definability.

We look at the separation problem for the class of languages defined by usual first order logic with order, successor when enriched with numerical predicates called modulo predicates.

We work with classes of languages directly, defining and using a technique called block abstraction, which actually shows how decidability of this problem transfers from fragments (or logically defined subclasses) of FO to their corresponding modulo enriched fragments. Finally we show block abstraction corresponds exactly to adding modulo predicates to the logic.

11h15-11h45 Pause café

11h45-12h15 **Charles Paperman** *Continuity and rational functions*
slides

—

12h30-14h00 Repas au restaurant Buffon

—

14h00-14h30 **Daniela Petrisan** *Minimization of transducers*
slides

14h30-15h00 **Thomas Colcombet** *On monoids for outputs*
slides

15h15-15h45 **Dimitri Gallois** *String Parallel Rewriting: analysis of the structure of the derivations*
slides

16h00-16h30 **Pierre Ohlmann** *Deciding emptiness of quantitative tree automata using proof systems*
slides

We will start by giving a simple proof system that allows to decide emptiness of parity tree automata, then explain how it can be extended to subzero automata. This is joint work with Nathanaël Fijalkow and Olivier Serre.

—

## DELTA Meeting in Porquerolles: 17-20 October 2017

See the official meeting page for details.

—

## DELTA Kickoff Meeting in Bordeaux: 9-10 February 2017

See the official meeting page for details.