Loading…

Approximate Comparison of Functions Computed by Distance Automata

Distance automata are automata weighted over the semiring ( ℕ ∪ { ∞ } , min , + ) (the tropical semiring). Such automata compute functions from words to ℕ ∪ { ∞ } . 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...

Full description

Saved in:
Bibliographic Details
Published in:Theory of computing systems 2016-05, Vol.58 (4), p.579-613
Main Authors: Colcombet, Thomas, Daviaud, Laure
Format: Article
Language:English
Subjects:
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Distance automata are automata weighted over the semiring ( ℕ ∪ { ∞ } , min , + ) (the tropical semiring). Such automata compute functions from words to ℕ ∪ { ∞ } . 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.
ISSN:1432-4350
1433-0490
DOI:10.1007/s00224-015-9643-3