Computing $\vec{\mathcal{S}}$-DAGs and Parity Games

TL;DR

This work introduces $\vec{\mathcal{S}}$-DAG-width, a directed width parameter that generalizes DAG-width and relates to non-monotone cops-and-robber strategies and directed tangles. It provides (i) an algorithm to compute a minimum-width $\vec{\mathcal{S}}$-DAG for any digraph and (ii) a polynomial-time method for solving parity games on digraphs with bounded $\vec{\mathcal{S}}$-DAG-width, extending Berwanger et al.'s results to the finer width measure. The core approach uses a specialized cops-and-robber game to characterize width and then adapts frontier-based parity-game solvers to the $\vec{\mathcal{S}}$-DAG framework, yielding practical algorithmic tools. The findings broaden the applicability of directed width theory and open avenues for efficient verification tasks on graphs constrained by $\vec{\mathcal{S}}$-DAG-width.

Abstract

Treewidth on undirected graphs is known to have many algorithmic applications. When considering directed width-measures there are much less results on their deployment for algorithmic results. In 2022 the first author, Rabinovich and Wiederrecht introduced a new directed width measure, $\vec{\mathcal{S}}$-DAG-width, using directed separations and obtained a structural duality for it. In 2012 Berwanger~et~al.~solved Parity Games in polynomial time on digraphs of bounded DAG-width. With generalising this result to digraphs of bounded $\vec{\mathcal{S}}$-DAG-width and also providing an algorithm to compute the $\vec{\mathcal{S}}$-DAG-width of a given digraphs we give first algorithmical results for this new parameter.

Figures (7)

• Figure 1: This figure illustrates the structure of the sets making up a separation. The arrows indicate that there can be edges from $V_{\top}$ to $V_{\bot}$ but not in the other direction.
• Figure 2: This figure illustrates the different types of robber initiative game states. For a single separator robber initiative game state the cop player chooses vertices for the cops to move to, such that all newly chosen cops are in the former range of the robber \ref{['item:C1:progressInReach']}. To leave the robber no way to escape, the remaining cops in $X_{\bot}$ restrict that range \ref{['item:C1:botBlocks']}. For a double separator robber initiative game state the cop player chooses two different sets $S_{1}$ and $S_{2}$ of vertices for the cops to move to. These sets represent two separations whose lower uncrossing has the separator $X_{\bot} \subseteq X$. \ref{['item:C2:containIntersection']} ensures that $X_{\bot}$ is indeed the separator of this uncrossing. \ref{['item:C2:realProgress', 'item:C2:separatorPartBelow']} yield that for every vertex the robber can move to, one of the two separations restricts the robbers range. By \ref{['item:C2:botBlocks']} the uncrossing restricts the range of the robber ensuring that the robber does not escape.
• Figure 3: This figure illustrates the process of deleting an edge $(v,w_2)$ and all newly resulting sources ($w_2,t_6,t_7$) as an example for the process in the proof for \ref{['niceExists']}. The part of the graph that is deleted is in red. The bottom separation for $v$ is unchanged as $\sigma((v,w_1)) \leq \sigma((v,w_2))$ and thus $\bot^{(T,\sigma)}(v) = \sigma((v,w_1)) \wedge \sigma((v,w_2)) = \sigma((v,w_1))$. For all remaining vertices the top separations are unchanged as their incoming edges still have their original top separations assigned to them.
• Figure 4: This figure illustrates the process of finding a forward facing vertex for a game state $p=(X, r)$ from the cop choice vertex $t$ for $r$ under $p_{-1}$. The red circled cop choice vertex $t$ is a child of the forward facing vertex $\hat{f}$(in blue) of the last cop initiative game state $p_{-2}$. In light orange is the DAG $T_{t,r,X}$, which contains all vertices $v$ starting from $t$ which lie above $\mathsf{R}_{D \setminus X}(r)$ meaning that $\mathsf{R}_{D \setminus X}(r) \subseteq V_{\bot}(\bot^{(T,\sigma)}(v))$. All sinks of this DAG are marked in pink. These sinks $\hat{f}'_1$ and $\hat{f}'_2$ are the possible choices for the forward-facing vertex for $p$.
• Figure 5: This figure illustrates the process of finding a forward facing vertex for a game state $p=(X, r)$ from the cop choice vertex $t$ for $r$ under $p_{-1}$. The red circled cop choice vertex $t$ is a child of the forward facing vertex $\hat{f}$(in blue) of the last cop initiative game state $p_{-2}$. In green is the DAG $T_{t,r,X}$, which contains all vertices $v$ starting from $t$ which lie above $\mathsf{R}_{D \setminus X}(r)$ meaning that $\mathsf{R}_{D \setminus X}(r) \subseteq V_{\bot}(\bot^{(T,\sigma)}(v))$. All sinks of this DAG are marked in pink. These sinks $\hat{f}'_1$ and $\hat{f}'_2$ are the possible choices for the forward-facing vertex for $p$.

Theorems & Definitions (43)

• Proposition 1.0
• Proposition 1.0
• Definition 2.1
• proof
• Lemma 2.3
• proof
• Definition 3.1: $\vec{\mathcal{S}}$-DAG cops-and-robber game
• Lemma 3.2
• proof
• Lemma 3.3