Comportements asymptotiques des automates Max-plus et Min-plus / Laure Daviaud ; sous la direction de Jean-Eric Pin et Thomas Colcombet

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 2014

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Théorie des automates mathématiques

Matrices

Approximation, Théorie de l'

Colcombet, Thomas (Directeur de thèse / thesis advisor)

Pin, Jean-Éric (Directeur de thèse / thesis advisor)

Université Paris Diderot - Paris 7 (1970-2019) (Organisme de soutenance / degree-grantor)

École doctorale Sciences mathématiques de Paris centre (Paris ; 2000-....) (Organisme de soutenance / degree-grantor)

Relation : Comportements asymptotiques des automates Max-plus et Min-plus / Laure Daviaud ; sous la direction de Jean-Eric Pin et Thomas Colcombet / Lille : Atelier national de reproduction des thèses , 2014

Résumé / Abstract : Ce mémoire porte sur l'étude de problèmes qui se situent à la frontière de décidabilité entre la décidabilité de l'existence de bornes et l'indécidabilité de la comparaison de fonctions. Pour cela, ce mémoire donne une description fine des fonctions calculées par automates min-plus et max-plus. Plus précisément, étant donnée une fonction f calculée 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. 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. Le théorème d'approximation du rapport fonction-longueur à une application à la comparaison approchée de fonctions calculées par automates min-plus. La comparaison obtenue 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 exhibe un algorithme qui permet de calculer un équivalent asymptotique de la longueur de la plus longue exécution dans le modèle de la size-change abstraction.

Résumé / Abstract : This thesis focuses on the study of issues that lie at the boundary between decidability of boundedness and undecidability of the comparison. For that, this paper gives a detailed description of functions computed by min-plus and max-plus automata.More precisely, given a function f computed by a min-plus (resp. max-plus) automaton, the main contribution of the thesis consists in the description of the function g that associates an integer n to the maximum of the values f(w) for words w of length less than n (respectively the minimum of the values f(w) for words w of length greater than n). The theorem for approximating the function-length ratio gives an approximation of the upper bound of ratios g(n)/n in the case of a min-plus automaton, and an approximation of the lower bound of ratios g(n)/n in the case of a max-plus automaton. The asymptotic equivalence theorem describes the asymptotic behavior of the function g in the case of max-plus automata and more precisely, it states that this function is asymptotically equivalent to a rational function. The theorem for approximating the function-length ratio has an application to the approximate comparison of min-plus automata. This approximate comparison highly refines previously known results about comparison, and appears to be the most accurate comparison between two functions computed by min-plus automata, that remains decidable. The asymptotic equivalence theorem exhibits an algorithm that calculates an asymptotic equivalent of the length of the longest run in a size-change abstraction instance.