Krishnendu Chatterjee ; Thomas A. Henzinger ; Rasmus Ibsen-Jensen ; Jan Otop - Edit Distance for Pushdown Automata

lmcs:3927 - Logical Methods in Computer Science, September 13, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:23)2017
Edit Distance for Pushdown AutomataArticle

Authors: Krishnendu Chatterjee ; Thomas A. Henzinger ; Rasmus Ibsen-Jensen ORCID; Jan Otop ORCID

    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.


    Volume: Volume 13, Issue 3
    Published on: September 13, 2017
    Accepted on: September 13, 2017
    Submitted on: September 13, 2017
    Keywords: Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • Quantitative Reactive Modeling; Funder: European Commission; Code: 267989
    • Quantitative Graph Games: Theory and Applications; Funder: European Commission; Code: 279307
    • Formal methodes for the design and analysis of complex systems; Funder: European Commission; Code: Z 211
    • Modern Graph Algorithmic Techniques in Formal Verification; Funder: European Commission; Code: P 23499

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1445 times.
    This article's PDF has been downloaded 335 times.