Edit distance for timed automata
Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Rupak Majumdar · 2014
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.