Robustness Analysis of String Transducers

Many important functions over strings can be represented as finite-state string transducers. In this paper, we present an automatatheoretic technique for algorithmically verifying that such a function is

robust

to uncertainty. A function encoded as a transducer is defined to be robust if for each small (i.e., bounded) change to any input string, the change in the transducer’s output is proportional to the change in the input. Changes to input and output strings are quantified using weighted generalizations of the Levenshtein and Manhattan distances over strings. Our main technical contribution is a set of decision procedures based on reducing the problem of robustness verification of a transducer to the problem of checking the emptiness of a reversal-bounded counter machine. The decision procedures under the generalized Manhattan and Levenshtein distance metrics are in

Pspace

and

Expspace

, respectively. For transducers that are Mealy machines, the decision procedures under these metrics are in

Nlogspace

and

Pspace

, respectively.