Laure Daviaud

The shortest identities for max-plus automata with two states, with M.Johnson, in MFCS 2017 - preprint

    Max-plus automata are quantitative extensions of automata designed to associate an integer with every non empty word. A pair of distinct words is said to be an identity for a class of max-plus automata if each of the automata in the class computes the same value on the two words. We give the shortest identities holding for the class of max-plus automata with two states. For this, we exhibit an interesting list of necessary conditions for an identity to hold. Moreover, this result provides a counter-example of a conjecture of Izhakian, concerning the minimality of certain identities.

Comparison of max-plus automata and joint spectral radius of tropical matrices, with P.Guillon and G.Merlet, in MFCS 2017 - preprint

    Weighted automata over the tropical semiring Zmax are closely related to finitely generated semigroups of matrices over Zmax. In this paper, we use results in automata theory to study two quantities associated with sets of matrices: the joint spectral radius and the ultimate rank. We prove that these two quantities are not computable over the tropical semiring, i.e. there is no algorithm that takes as input a finite set of matrices S and provides as output the joint spectral radius (resp. the ultimate rank) of S. On the other hand, we prove that the joint spectral radius is nevertheless approximable and we exhibit restricted cases in which the joint spectral radius and the ultimate rank are computable. To reach this aim, we study the problem of comparing functions computed by weighted automata over the tropical semiring. This problem is known to be undecidable, and we prove that it remains undecidable in some specific subclasses of automata.

Which classes of origin graphs are generated by transducers?, with M.Bojanczyk, B.Guillon and V.Penelle, in ICALP 2017 - preprint

    We study various models of transducers equipped with origin information. We consider the semantics of these models as particular graphs, called origin graphs, and we characterise the families of such graphs recognised by streaming string transducers.

Degree of sequentiality of weighted automata, with P-A.Reynier, I.Jecker and D.Villevalois, in FOSSACS 2017 - preprint

    Weighted automata (WA) are an important formalism to describe quantitative properties. Obtaining equivalent deterministic machines is a longstanding research problem. In this paper we consider WA with a set semantics, meaning that the semantics is given by the set of weights of accepting runs. We focus on multi-sequential WA that are defined as finite unions of sequential WA. The problem we address is to minimize the size of this union. We call this minimum the degree of sequentiality of (the relation realized by) the WA. For a given positive integer k, we provide multiple characterizations of relations realized by a union of k sequential WA over an infinitary finitely generated group: a Lipschitz-like machine independent property, a pattern on the automaton (a new twinning property), and a subclass of cost register automata. When possible, we effectively translate a WA into an equivalent union of k sequential WA. We also provide a decision procedure for our twinning property for commutative computable groups thus allowing to compute the degree of sequentiality. Last, we show that these results also hold for word transducers and that the associated decision problem is Pspace-complete.

A Generalised Twinning Property for Minimisation of Cost Register Automata, with P-A.Reynier and J-M.Talbot, in LICS 2016 - preprint

    Weighted automata (WA) extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata (CRA) have been introduced as an alternative model to describe any function realised by a WA by means of a deterministic machine.
    Unambiguous WA over a monoid (M,.) can equivalently be described by cost register automata whose registers take their values in M, and are updated by operations of the form X:=Y.c, with c in M. This class is denoted by CRA(.c,M).
    We introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k=1. Given an unambiguous weighted automaton W over an infinitary group (G,.) realizing some function f, we prove that the three following properties are equivalent:
i) W satisfies the twinning property of order k,
ii) f satisfies the k-bounded variation property,
iii) f can be described by a CRA(.c,M) with at most k registers.
    In the spirit of tranducers, we actually prove this result in a more general setting by considering machines over the semiring of finite sets of elements from (G,.): the three properties are still equivalent for such finite-valued weighted automata, that is the ones associating with words subsets of G of cardinality at most l, for some natural l. Moreover, we show that if the operation . of G is commutative and computable, then one can decide whether a WA satisfies the twinning property of order k. As a corollary, this allows to decide the register minimisation problem for the class CRA(.c,M).
    Last, we prove that a similar result holds for finite-valued finite-state transducers, and that the register minimisation problem for the class CRA(.c,B*) is PSPACE-complete.

Varieties of cost functions, with D.Kuperberg and J-É.Pin, in STACS 2016 - preprint

    Regular cost functions were introduced as a quantitative generalisation of regular languages, retaining many of their equivalent characterisations and decidability properties. For instance, stabilisation monoids play the same role for cost functions as monoids do for regular languages. The purpose of this article is to further extend this algebraic approach by generalising two results on regular languages to cost functions: Eilenberg's varieties theorem and profinite equational characterisations of lattices of regular languages. This opens interesting new perspectives, but the specificities of cost functions introduce difficulties that prevent these generalisations to be straightforward. In contrast, although syntactic algebras can be defined for formal power series over a commutative ring, no such notion is known for series over semirings and in particular over the tropical semiring.

Classes of languages generated by the Kleene star of a word, with C.Paperman, in MFCS 2015 - preprint

    Equational descriptions of regular languages is a successful and long-standing approach to obtain characterisations of classes of regular languages. One of the first result is the one of Schützenberger on aperiodic monoids. In the case of varieties of regular languages, the Reitermann Theorem guarantees the existence of a characteristic set of profinite equations. This theorem has been extended to several kinds of classes of languages, including lattices and Boolean algebras.
    The aim of this paper is to study the four classes of regular languages obtained respectively as the lattice, Boolean algebra, lattice closed under quotient and Boolean algebra closed under quotient generated by the class of all languages of the form u*, where u is a word.
    Our main result is an equational characterisation for each of these four classes. These equational characterisations being effective, they give as a counterpart the decidability of the membership problem: One can decide whether a given regular language belongs to one of these classes. In addition, our results also provide a general form for the languages belonging to each of these classes.

Size-change abstraction and max-plus automata, with T.Colcombet and F.Zuleger, in MFCS 2014 - preprint

    Max-plus automata are automata weighted over the semiring (N,max,+). More precisely a max-plus automaton is a non deterministic finite automaton with a weight (a non-negative integer) on each transition. The weight of a given run is the sum of the weights of the transitions along the run and the weight of a word w is the maximum of the weights of the runs labelled by w and going from an initial state to a final state. Thus max-plus automata compute functions from the set of words to the set of non-negative integers.
    We are interested in studying the asymptotic behaviour of these functions and more precisely in describing the function that minimises the behaviour of max-plus automata with respect to the length of the words. We prove that given a max-plus automaton computing a function f, if the function g defined by g(n)=min{f(w)| |w|> n} is not equal to -infinity, then there is a rationnal q in [0,1] such that g is asymptotically equivalent to n^q. Moreover this rationnal is computable.
    This result can, in combination with the size-change abstraction, be used for inferring the termination time of an algorithm as a function of the size of its input.

Approximate comparison of distance automata, with T.Colcombet, in STACS 2013, in Theory of Computing Systems (ToCS) - preprint

    Distance automata are automata weighted over the tropical semiring (the set of positive integers and +infinity, equipped with operations min and +). Such an automaton computes a function from the set of words to the set of positive integers and +infinity such as the number of occurrences of a given letter. It is known that testing f < g is an undecidable problem for f and g computed by distance automata. The main contribution of this paper is to show that an approximation of this problem becomes decidable.
    We present an algorithm which, given e>0 and two functions f,g computed by distance automata, outputs "yes" if f < (1-e)g, "no" if there is a word w such that f(w)>g(w), and may answer "yes" or "no" in all other cases. This result highly refines previously known decidability results of the same type.
    The core argument behind this quasi-decision procedure is an algorithm which is able to provide an approximated finite presentation to the closure under products of sets of matrices over the tropical semiring.
    We also provide another theorem, of affine domination, which shows that previously known decision procedures for cost-automata have an improved precision when used over distance automata.

PhD thesis

Comportements asymptotiques des automates max-plus et min-plus - manuscript (in French)

    Min-plus and max-plus automata are non deterministic finite automata with weights (non-negative integers) on their transitions. These automata compute functions from the set of words to the set of non negative integers including an infinite value.
    Questions such as equivalence or comparison are undecidable problems. This implies the impossibility to precisely describe the evolution of these functions.
    This thesis gives results about the description and approximation of the asymptotic behaviours of these functions. More precisely, given a function f computed by a min-plus (resp. max-plus) automaton, we consider a function from the set of positive integers defined by g:n -> max{f(w) | |w| min{f(w) | |w|>n}.
    First, the asymptotic behaviour of g is of the form n^q where q is a rationnal from [0,1]. Secondly, it is possible to approximate the ratio g(n)/n.
    These questions are related with the approximation of sets of matrices over the min-plus (resp. max-plus) semiring.

Résumé de la thèse :

    L’informatique théorique porte sur l'étude de modèles de calcul dont il s’agit de décrire le comportement et les propriétés. Ces modèles sont notamment utilisés pour la spécification et la vérification de programmes. En connaitre les propriétés permet à la fois de s’assurer de leur bon comportement mais aussi de minimiser le temps et la quantité de ressources nécessaires pour faire un calcul. Un des modèles de calcul les plus simples est le modèle des automates finis non déterministes. La théorie des automates finis, initiée dans les années 1950 est très riche et a été largement étudiée. Elle a de nombreux intérêts : les automates finis sont déterminisables, la classe des langages qu’ils définissent, les langages rationnels, a de bonnes propriétés de clôture et de décidabilité et il en existe des équivalents logiques et algébriques. Néanmoins, le comportement d’un automate sur un mot est une notion purement qualitative: le mot est accepté ou rejeté. On voit alors assez vite la nécessité d’ajouter une dimension quantitative. Que faire, par exemple, si on veut compter le nombre de chemins acceptants étiqueté par un mot donné ?

Automates min-plus et automates max-plus

    Les automates min-plus et max-plus et de manière générale les automates pondérés (ou automates à multiplicités) sont une manière d’ajouter cette dimension quantitative aux automates en pondérant les transitions. Ils ont été introduits par Schützenberger et généralisés par Eilenberg. L’idée d’un automate pondéré est d’associer à chaque mot, non plus une valeur booléenne, mais une valeur dans un ensemble donné, par exemple l’ensemble des entiers ou celui des réels. Plus précisément, un automate pondéré calcule une fonction de l’ensemble des mots dans un semi-anneau. Les automates min-plus et les automates max-plus sont des automates finis non déterministes dont chaque transition est pondérée. En fonction du contexte, ces poids peuvent être des valeurs entières, rationnelles ou réelles, positives ou négatives. Ce mémoire ne considère que des pondérations entières positives. L’idée d’un automate min-plus est donc de mettre un coût, représenté par un entier positif, sur chaque transition. Le long d’un chemin les coûts des transitions s’additionnent. On choisit ensuite le chemin de coût minimal. De même pour un automate max-plus, il s’agit de mettre un gain sur chaque transition. Quand on parcourt un chemin, on additionne les gains, puis on choisit le chemin qui maximise le gain. Plus précisément, chaque transition de l’automate a un poids, le poids d’un chemin est la somme des poids des transitions qui composent le chemin, un chemin est acceptant s’il commence dans un état initial et se termine dans un état final, et un automate min-plus (resp. max-plus) associe à un mot w le minimum (resp. le maximum) des poids des chemins acceptants étiquetés par w. Les automates min-plus ont été utilisés pour résoudre de nombreux problèmes sur les langages rationnels : le problème de la puissance finie, le problème de la hauteur d'étoile, le problème de la complexité non-déterministe (essentiellement compter le nombre de choix non-déterministes faits par un automate sur la lecture d’un mot). Les automates min-plus et max-plus ont ainsi des applications à la théorie des langages formels. Ils ont également des applications dans des problèmes d’optimisation et de vérification, de description des systèmes à événements discrets et de reconnaissance automatique du langage.

Description des fonctions calculées

    Résoudre les problèmes mentionnés ci-dessus pose la question de la description du comportement des fonctions calculées par automates min-plus et max-plus : existence de bornes, équivalence, comparaison… Du côté des résultats négatifs, l’équivalence et la comparaison de fonctions calculées par automates min-plus ou max-plus ont été montrées indécidables par Krob en 1992 : il est indécidable de savoir si deux automates max-plus (resp. min-plus) calculent la même fonction ou de comparer ces fonctions (à savoir est-ce que pour tout mot w, f(w) < g(w) ?). A l’inverse, on peut citer deux résultats positifs en terme de décidabilité : l’existence de bornes est décidable (Hashiguchi 1978 pour les automates min-plus) ainsi que le domination polynomiale : étant données des fonctions f et g calculées par automates min-plus (resp. max-plus), le problème de savoir s’il existe un polynôme P tel que f < Pog est décidable (Colcombet 2009). Ainsi, il n’est pas possible de décider la comparaison précise des fonctions calculées par automates max-plus et min-plus. On obtient néanmoins cette décidabilité si on relâche suffisamment les hypothèses et que l’on accepte une erreur polynomiale.

Contributions de la thèse

    Ce mémoire porte sur l’étude de problèmes qui se situent à la frontière de la décidabilité entre les problèmes mentionnés ci-dessus et donne une description fine des fonctions calculées par automates min-plus et max-plus. Plus précisément, étant donnée une fonction calculée f par un automate min-plus (resp. max-plus) la contribution principale du mémoire consiste en la description de la fonction g qui, à un entier n, associe le maximum des valeurs f(w) pour les mots w de longueurs inférieures à n (resp. le minimum des valeurs f(w) pour les mots w de longueurs supérieures à n).
    Le théorème d’approximation du rapport fonction-longueur donne une approximation de la borne supérieure des rapports g(n)/n dans le cas d’un automate min-plus, et une approximation de la borne inférieure des rapports g(n)/n dans le cas d’un automate max-plus. Plus précisément, pour toute erreur e>0, il est possible d’approximer ces valeurs à e-près. Ce résultat donne alors un algorithme permettant de comparer deux fonctions calculées par des automates min-plus à e-près : il existe un algorithme, qui étant données f et g calculées par des automates min-plus et un réel e>0, répond : oui si f < g, non s’il existe un mot w tel que f(w) > (1+e)g(w), indifféremment oui ou non dans les autres cas. Cette comparaison raffine grandement les résultats déjà connus sur la comparaison de fonctions, et semble être la comparaison la plus précise qui reste décidable entre deux fonctions calculées par automates min-plus.
    Le théorème d’équivalence asymptotique décrit le comportement asymptotique de la fonction g dans le cas max-plus, et plus précisément, il est prouvé que cette fonction est asymptotiquement équivalente à une fonction rationnelle. Ce résultat s’applique en vérification dans le calcul de complexité d’une abstraction de programme : le modèle de la size-change abstraction. On exhibe un algorithme qui permet de calculer un équivalent asymptotique de la longueur de la plus longue exécution dans cette abstraction de programme.