Delta logoANR

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,

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

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

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

I will discuss an ongoing work, which is to understand Generative Adversarial Network in the context of weighted automata.

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

We introduce a class of transformations of finite data words generalizing the well-known class of regular finite string transformations described by MSO-definable transductions of finite strings. These transformations map input words to output words whereas our transformations handle data words where each position has a letter from a finite alphabet and a data value. Each data value appearing in the output has as origin a data value in the input. As is the case for regular transformations we show that our class of transformations has equivalent characterizations in terms of deterministic two-way and streaming string transducers.

Joint work with Antoine Durand-Gasselin

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

This talk is about 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

The equivalence problem for two-way transducers is known to decidable in the functional case, but it is undecidable if the transducer is not functional (and this even in the one-way case). We show that under the origin semantics introduced by Bojanczyk, equivalence is again decidable for non-functional, two-way transducers.

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

A natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, whose runs are described by regular lan- guages L over {1, 2} × A, where (i, a) is interpreted as reading letter a from tape i. Accordingly, a word w ∈ L denotes the pair (u1, u2) ∈ A∗ × A∗ in which ui is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, which we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1, 2}. In this way, for each regular language C ⊆ {1, 2}∗, one obtains a class Rel(C) of relations. Regular, Recognizable, and length-preserving relations are all examples of classes that can be defined in this way. We study the problem of containment for synchronized classes of relations: given C, D ⊆ {1, 2}∗, is Rel(C) ⊆ Rel(D)? We show a characterization in terms of C and D which gives a decidability procedure to test for class inclusion. This also yields a procedure to re-synchronize languages from {1, 2} × A preserving the denoted relation whenever the inclusion holds.

15h30-16h00 Pause café

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

In this talk I present a logic, called LT, to express properties of transductions, i.e. binary relations from input to output (finite) words. I argue that LT is a suitable candidate as a specification language for verification of non reactive systems, extending the successful approach of verifying synchronous systems via Mealy Machines and MSO.

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.

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

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

Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Cerny in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decidable equivalence problem (in PSpace).

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

We investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is NP-ccomplete. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. We show that non-emptiness of two-way visibly pushdown Parikh automata which are single-use is NExpTime-ccomplete. We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.

10h45-11h15 Pause café

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

The robustness of the famous compression algorithm of Lempel and Ziv is still not well understood: in particular, until now it was unknown whether the addition of one bit in front of a compressible word could make it incompressible. This talk will answer that question, advertised by Jack Lutz under the name “one-bit catastrophe” and which has been around since at least 1998. We will show that a “well” compressible word remains compressible when a bit is added in front of it, but some “few” compressible words indeed become incompressible.

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

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

A function (or more generally a transduction) is said to be 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

Classical results from algebra, such as Hilbert's Basis Theorem and Hilbert’s Nullstellensatz, have been used to decide equivalence for some classes of transducers, such as HDT0L (Honkala 2000) or more recently deterministic tree-to-string transducers (Seidl, Maneth, Kemper 2015). In this talk, we propose an abstraction of these methods. The goal is to investigate the scope of the “Hilbert method” for transducer equivalence that was described above.

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:

  1. We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.
  2. 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

The containment problem for quantitative automata is the natural quantitative generalisation of the classical language inclusion problem for Boolean automata. We study it for probabilistic automata, where it is known to be undecidable in general. We restrict our study to the class of probabilistic automata with bounded ambiguity. There, we show decidability (subject to Schanuel's conjecture) when one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Furthermore, we show that this is close to the most general decidable fragment of this problem by proving that it is already undecidable if one of the automata is allowed to be linearly ambiguous.

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

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

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

Joint work with Thomas Place.

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

The separation problem for a class C is: given two regular languages L_1 and L_2, is there a language L in C which contains L_1 and is disjoint from L_2?

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

A word-to-word function is continuous for a class of languages V if its inverse maps V languages to V. This notion provides a basis for an algebraic study of transducers, and was integral to the characterization of the sequential transducers computable in some circuit complexity classes. Here, I will expose some results on the decidability of continuity for functional transducers and some standard classes of regular languages.

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

We study the notion of parallel rewriting for words, i.e allowing to rewrite non conflicting part of a word at once. If this notion has been studied in the context of terms mainly for proving confluence properties, there are no works to our knowledge that study the structure of parallel rewriting derivations. In this paper, we first introduce a notion of graph capturing the essence of a finite derivation. Thus we consider parallel rewriting derivations when the number of possible steps is bounded by k or when the possible derived words are derivable in at most k number of steps. Such parallel systems have interesting properties such that the defining a rational function. We propose different subcases when there exists an algorithm to decide if a set of rules define bounded derivations. Finally, we exhibit some relations between string rewriting systems and the chase, a graph rewriting procedure very useful in the fields of database and knowledge representation.

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

Quantitative tree automata extend parity tree automata by adding new conditions for a run to be accepting. For instance, it may be asked that the set of branches with maxinf in a given subset of states has zero measure. Decidability of the emptiness problem for such classes of automata has recently been shown, using well-tuned parity games. We discuss a different approach based on a proof system.

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.

See the official meeting page for details.

See the official meeting page for details.