Strategic Dominance: A New Preorder for Nondeterministic Processes

TL;DR

This work introduces strategic dominance, a novel refinement notion between trace inclusion and tree-like simulation for nondeterministic state-transition models, formalized via a resolver-based game where every deterministic implementation of A is matched by a strategy in B. It defines resolver logic, a decidable first-order extension of Presburger arithmetic that quantifies over infinite words and resolvers, and shows how model checking resolver logic yields a 2-ExpTime decision procedure for strategic dominance and related relations. The paper also develops eight resolver relations, proves a hierarchy and separating examples among them, and applies resolver logic to compute bottom values, assess history-determinism, and decide hyperproperty inclusion. These results provide a unifying, logic-based approach to analysis of boolean and quantitative automata, with practical implications for co-safety/co-liveness, history-determinism, and hyperproperty reasoning. Overall, resolver logic offers a powerful framework for verifying refinement concepts and hyperproperties in complex automata-theoretic settings.

Abstract

We study the following refinement relation between nondeterministic state-transition models: model B strategically dominates model A iff every deterministic refinement of A is language contained in some deterministic refinement of B. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between A and B: every strategy that resolves the nondeterminism of A is dominated by a strategy that resolves the nondeterminism of B. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.

Figures (6)

• Figure 1: A $\mathsf{LimSup}$-automaton $\mathcal{A}\xspace$ over $\Sigma = \{a,b\}$ with $R^{\text{pos}}(\mathcal{A}\xspace) \subsetneq R^{\text{fin}}(\mathcal{A}\xspace) \subsetneq R(\mathcal{A}\xspace)$.
• Figure 2: Two $\mathsf{LimSup}$-automata $\mathcal{A}\xspace$ and $\mathcal{B}\xspace$ and the product $\mathcal{A}\xspace \times_1 \mathcal{B}\xspace$.
• Figure 3: Left: The definitions of inclusion (denoted ${\mathrel{\subseteq}}$), simulation (denoted ${\mathrel{\preceq}}$), and the resolver relations we study in \ref{['sec:resolverrelations']} including strategic dominance (denoted ${\mathrel{\trianglelefteq}}$). Right: The implications between these relations as proved in \ref{['cl:inclusion', 'cl:simulation', 'cl:implications', 'cl:restrictedresolvers', 'cl:counterexamples', 'cl:corollary']}.
• Figure 4: Two automata $\mathcal{A}\xspace$ and $\mathcal{B}\xspace$ such that $\mathcal{A}\xspace \mathrel{\subseteq}^{\text{pos}} \mathcal{B}\xspace$ but $\mathcal{A}\xspace \not\mathrel{\trianglelefteq}^{\text{pos}} \mathcal{B}\xspace$. Note that $\mathcal{A}\xspace$ and $\mathcal{B}\xspace$ can be $\mathsf{Inf}$-, $\mathsf{Sup}$-, $\mathsf{LimSup}$-, or $\mathsf{LimInf}$-automata as well as safety, reachability, Büchi, or coBüchi automata. The exact values of the omitted weights depend on the considered value function. For example, we can take as weight 1 for $\mathsf{Inf}$ and 0 for $\mathsf{Sup}$ while both choices work for $\mathsf{LimSup}$ and $\mathsf{LimInf}$.
• Figure 5: Two automata $\mathcal{A}\xspace$ and $\mathcal{B}\xspace$ such that (i) $\mathcal{A}\xspace \mathrel{\trianglelefteq}^{\text{pos}} \mathcal{B}\xspace$ but $\mathcal{A}\xspace \not\mathrel{\preceq}^{\text{pos}} \mathcal{B}\xspace$, (ii) $\mathcal{A}\xspace \mathrel{\preceq}^{\text{pos}} \mathcal{A}\xspace$ but $\mathcal{A}\xspace \not\mathrel{\hbox{$\leq$$\blacktriangleleft$}}_{\times}^{\text{pos}} \mathcal{A}\xspace$, and (iii) $\mathcal{B}\xspace \mathrel{\hbox{$\leq$$\blacktriangleleft$}}_{\times}^{\text{pos}} \mathcal{A}\xspace$ but $\mathcal{B}\xspace \not\mathrel{\hbox{$\leq$$\blacktriangleleft$}}^{\text{pos}} \mathcal{A}\xspace$. The transitions that are not shown lead to a sink state with a self-loop on every letter with weight 0. Note that $\mathcal{A}\xspace$ and $\mathcal{B}\xspace$ can be $\mathsf{Inf}$-, $\mathsf{Sup}$-, $\mathsf{LimSup}$-, or $\mathsf{LimInf}$-automata as well as safety, reachability, Büchi, or coBüchi automata. The exact values of the omitted weights depend on the considered value function. For example, we can take as weight 1 for $\mathsf{Inf}$ and 0 for $\mathsf{Sup}$ while both choices work for $\mathsf{LimSup}$ and $\mathsf{LimInf}$.

Theorems & Definitions (27)

• Definition 1: automaton
• Definition 2: resolver
• Example 3
• Definition 4: partial resolver
• Definition 5: synchronized product
• Example 6
• Remark 7
• Remark 8
• Lemma 9
• Proposition 10