Approximate comparison of functions computed by distance automata

Thomas Colcombet, Laure Daviaud

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


Distance automata are automata weighted over the semiring (Formula presented.) (the tropical semiring). Such automata compute functions from words to (Formula presented.). It is known from Krob that the problems of deciding ‘ f≤g’ or ‘ f=g’ for f and g computed by distance automata is an undecidable problem. The main contribution of this paper is to show that an approximation of this problem is decidable. We present an algorithm which, given ε>0 and two functions f,g computed by distance automata, answers “yes” if f≤(1−ε)g, “no” if f≦̸g, and may answer “yes” or “no” in all other cases. The core argument behind this quasi-decision procedure is an algorithm which is able to provide an approximated finite presentation of the closure under products of sets of matrices over the tropical semiring. Lastly, our theorem of affine domination gives better bounds on the precision of known decision procedures for cost automata, when restricted to distance automata.

Original languageEnglish
Pages (from-to)579-613
Number of pages35
JournalTheory of Computing Systems
Issue number4
Early online date11 Jul 2015
Publication statusPublished - 1 May 2016


  • Asymptotic behaviour
  • Comparison
  • Distance automata
  • Tropical semiring
  • Weighted automata

Cite this