Abstract

Towards capturing and measuring robustness of computations wrt to a desired specification, we look into the following questions:
1. Can we have a notion of an edit distance between infinite words, and if so, can it be efficiently computed?
2. Can we distill from an omega-regular language the natural preference relation that it induced?

The quest of answering the first question goes via a discussion on normalized edit distance between finite words. In particular, we show that the normalized edit distance (NED) of [Marzal and Vidal, 93] over uniform weights is a metric. We then provide a necessary and sufficient condition on a cost function d on edit operations so that the resulting measure NED_d between words would be a metric.
We further show that NED can be extended to a notion that applies to infinite words, call it \omega-NED, and that computing \omega-NED between words/languages can be done in polynomial time.

To answer the second question we show that we can refine the 5-valued semantics of [Tabuada & Neider, 2016] into an infinite-valued semantics that captures robustness. Towards this aim we provide natural colors to individual letters of an infinite word capturing whether that letter contributes positively or negatively to the robustness of the infinite word wrt to the language.

Based on joint works with Joshua Grogin, Oded Margalit, Elina Sudit, Ilay Tzarfati and Gera Weiss.

Video Recording