Omega-Regular Robustness

TL;DR

The paper addresses deriving a semantic, infinite-valued robustness relation for ω-regular specifications that is independent of representation. It develops a theoretical framework built on Wagner hierarchy and natural ranks to assign per-letter ranks and colors to ω-words, and constructs a pair of DPAs (the vigor DPA and the robustness DPA) that produce a robustness value for lassos in polynomial time. The key contributions include formal definitions of natural ranks, a color/score scheme for letters and infixes, and a constructive procedure to compute the robustness value via the robustness automaton; it also proves duality with the complement language. The framework refines prior multi-valued semantics and provides a principled basis for runtime guidance and analysis directly from the ω-regular specification, with potential practical impact in robust synthesis and verification.

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 $ω$-regular properties. Still, it seems there is a natural robustness preference relation induced by an $ω$-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 $ω$-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.

Figures (8)

• Figure 4.1: Parity automata $\mathcal{P}_1,\mathcal{P}_2,\mathcal{P}_3,\mathcal{P}_{L_{\infty ab}}^\text{\FourStar}$ for $L_{\infty ab}$.
• Figure :
• Figure B.1: Parity automata $\mathcal{P}_1,\mathcal{P}_2,\mathcal{P}_3$ for the languages $L_{\infty a}$, $L_{\textbf{G} a}$, and $L_{a\text{-seq}}$, respectively, annotated with accepting (dashed green) and rejecting SCCs (dashed red) witnessing their inclusion measure. Recall that $L_{a\text{-seq}}$ is $\infty a \wedge (\infty aa \to \infty aaa)$.
• Figure B.2: The precise parity automata $\mathcal{P}_{a\text{-seq}}^{\text{Precise}}$ and $\mathcal{P}_{\infty ab}^{\text{Precise}}$ for $L_{a\text{-seq}}$ and $L_{\infty ab}$ resp. over $\Sigma=\{a,b\}$.
• Figure B.3: The vigor DPA for $L_{\text{mod}2}=\infty a~\bigvee~(|w|_{a}$ is even $\wedge~\neg \infty c)~\bigvee~(|w|_{a}$ is odd $\wedge~\neg \infty b)$ over $\Sigma=\{a,b,c\}$, and the related components: $\mathcal{A}[\sim_{L_{\text{mod}2}}]$ induced by the equivalence classes of $L_{\text{mod}2}$, parity automata $\mathcal{P}{\varepsilon}^\text{\FourStarOpen}$ and $\mathcal{P}_{a}^\text{\FourStarOpen}$ for the respective languages, as per \ref{['def:rbst-dpa']}. There are two versions of the vigor DPA $\mathcal{P}^{\text{\FourStarOpen}}_{L_{\text{mod}2}}$ for $L_{\text{mod}2}$ : the one on the left shows the relation to the components as per \ref{['def:rbst-dpa']}, whereas the one on the right shows only the final ranks.

Theorems & Definitions (65)

• Example 1.1: Basic TN
• Example 1.2: Refined TN
• Example 3.4: Infinitely often
• Definition 4.1: Natural rank of an infinite word EhlersS22, slightly altered
• Example 4.2
• Definition 4.3: Natural rank of an infix BohnL24, slightly altered
• Example 4.4
• Remark 4.5
• Remark 4.5
• Definition 5.1: Influential index