Edit distance for pushdown automata

The edit distance between two words w1 , w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2 . The edit distance generalizes to languages L1, L2, where the edit distance from L1 to L2 is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k, and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite