一句话：完整刻画了下推自动机到有限自动机编辑距离的阈值判定与有限性判定的可判定性和复杂度。
编辑距离可推广到语言之间：从语言 L1 到 L2 的编辑距离是最小的 k，使得 L1 中每个词都能通过至多 k 次插入、删除和替换变为 L2 中的某个词。本文研究下推自动机及其子类之间的编辑距离计算问题。由于计算到下推自动机的编辑距离不可判定，本文将下推自动机视为带递归的程序实现，将有限自动机对应的正则语言视为规范，关注从下推自动机到有限自动机的编辑距离。作者给出了两个核心判定问题的完整可判定性与复杂度图景：给定阈值 k，判定编辑距离是否不超过 k；以及判定编辑距离是否为有限。该工作系统刻画了这些问题在自动机理论框架下的可判定性边界与复杂度分类。
The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists a word in $\mathcal{L}_2$ 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.Comment: An extended version of a paper accepted to ICALP 2015 with the same title. The paper has been accepted to the LMCS journal
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ChatterjeeHIO15,
title = {Edit Distance for Pushdown Automata},
author = {Krishnendu Chatterjee and Thomas A. Henzinger and Rasmus Ibsen-Jensen and Jan Otop},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:23)2017}
}