Krishnendu Chatterjee
ABSTRACT
The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition.
In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in time stamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than δ away from the parameter, for δ < 0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and analogous decidability results hold for rectangular automata.
- A. Aho and T. Peterson. A minimum distance error-correcting parser for context-free languages. SIAM J. of Computing, 1:305--312, 1972.Google Scholar
Cross Ref
- R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183--235, 1994. Google ScholarDigital Library
- M. Benedikt, G. Puppis, and C. Riveros. Regular repair of specifications. In LICS, pages 335--344. IEEE Computer Society, 2011. Google ScholarDigital Library
- R. Brenguier, S. Göoller, and O. Sankur. A comparison of succinctly represented finite-state systems. In CONCUR, pages 147--161, 2012. Google ScholarDigital Library
- K. Chatterjee and V. S. Prabhu. Quantitative timed simulation functions and refinement metrics for real-time systems. In HSCC, 2013. Google ScholarDigital Library
- A. Donzé, T. Ferrère, and O. Maler. Efficient robust monitoring of signal temporal logic. In CAV 2013, LNCS. Springer, 2013. Google ScholarDigital Library
- A. Donzé and O. Maler. Robust satisfaction of temporal logic over real-valued signals. In FORMATS, LNCS, pages 92--106. Springer, 2010. Google ScholarDigital Library
- G. Fainekos and G. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42), 2009. Google ScholarDigital Library
- G. Fainekos, S. Sankaranarayanan, K. Ueda, and H. Yazarel. Verification of automotive control applications using S-TaLiRo. In Proc. American Control Conference, 2012.Google ScholarCross Ref
- T. A. Henzinger and P. W. Kopke. Discrete-time control for rectangular hybrid automata. Theor. Comput. Sci., 221(1--2):369--392, June 1999. Google ScholarDigital Library
- J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Adison-Wesley Publishing Company, Reading, Massachusets, USA, 1979. Google ScholarDigital Library
- R. Karp. Mapping the genome: some combinatorial problems arising in molecular biology. In STOC 93, pages 278--285. ACM, 1993. Google ScholarDigital Library
- V. Levenshtein. Binary codes capable of correcting deletions, insertions and reversals. Soviet Physics-Doklady, 10:707--710, 1966.Google Scholar
- M. Mohri. Edit-distance of weighted automata: general definitions and algorithms. Intl. J. of Foundations of Comp. Sci., 14:957--982, 2003.Google ScholarCross Ref
- T. Okuda, E. Tanaka, and T. Kasai. A method for the correction of garbled words based on the levenshtein metric. IEEE Trans. Comput., 25:172--178, 1976. Google ScholarDigital Library
- J. Ouaknine and J. Worrell. Universality and language inclusion for open and closed timed automata. In O. Maler and A. Pnueli, editors, HSCC, volume 2623 of Lecture Notes in Computer Science, pages 375--388. Springer, 2003. Google ScholarDigital Library
- G. Pighizzini. How hard is computing the edit distance? Information and Computation, 165:1--13, 2001. Google ScholarDigital Library
- W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177--192, Apr. 1970. Google ScholarDigital Library
- R. A. Wagner. Order-n correction for regular languages. Commun. ACM, 17(5):265--268, 1974. Google ScholarDigital Library
- R. A. Wagner and M. J. Fischer. The string-to-string correction problem. J. ACM, 21(1):168--173, Jan. 1974. Google ScholarDigital Library
Index Terms
- Edit distance for timed automata
Recommendations
Edit distance neighbourhoods of input-driven pushdown automata
AbstractEdit distance ℓ-neighbourhood of a formal language is the set of all strings that can be transformed to one of the strings in this language by at most ℓ insertions and deletions. Both the regular and the context-free languages are ...
Input-driven pushdown automata for edit distance neighborhood
AbstractEdit distance ℓ-neighborhood of a language L is the set of all strings that can be obtained by at most ℓ elementary edit operations — deleting or inserting one symbol in the string — from some string in L. We shall show that if L is ...
Computing the edit distance of a regular language
The edit distance (or Levenshtein distance) between two words is the smallest number of substitutions, insertions, and deletions of symbols that can be used to transform one of the words into the other. In this paper, we consider the problem of ...
Comments