Omega-Regular Robustness

Abstract

Roughly speaking, a system is said to be robust if it can resist disturbances and still function correctly. For instance, if the requirement is that the temperature remains in an allowed range $[l,h]$, then a system that remains in a range $[l',h']\subset[l,h]$ is more robust than one that reaches $l$ and $h$ from time to time. In this example the initial specification is quantitative in nature, this is not the case in $\omega$-regular properties. Still, it seems there is a natural robustness preference relation induced by an $\omega$-regular property. E.g. for a property requiring that every request is eventually granted, one would say that a system where requests are granted two ticks after they are issued is more robust than one in which requests are answered ninety ticks after they are issued. In this work we manage to distill a robustness preference relation that is induced by a given $\omega$-regular language. The robustness preference relation is a semantic notion (agnostic to the given representation of the language) that relies on Wagner's hierarchy and on Ehlers and Schewe's definition of natural rank of infinite words. It aligns with our intuitions on common examples, satisfies some natural mathematical criteria, and refines Tabuada and Neider's five-valued semantics into an infinite domain.