Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Connectivity in the presence of an opponent

Zihui Liang, Bakh Khoussainov, Toru Takisaka, Mingyu Xiao

TL;DR

This work studies connectivity in Müller games by reducing connectivity solving to incremental SCC maintenance (ISCCM) through a derivative sequence, enabling two efficient ISCCM-based algorithms with parameterized runtimes that outperform naive bounds. It also delivers a rigorous, self-contained correctness proof for Horn's polynomial-time algorithm for explicitly given Müller games, showing how the connectivity subroutine underpins the broader solver. The two algorithms achieve favorable time complexities in sparse and dense regimes and, when combined with Horn-like reductions, substantially improve practical solvability of Müller games in model checking. Overall, the paper advances both theoretical understanding and algorithmic practicality for solving connectivity and Müller games, with direct implications for verification and synthesis pipelines.

Abstract

The paper introduces two player connectivity games played on finite bipartite graphs. Algorithms that solve these connectivity games can be used as subroutines for solving Müller games. Müller games constitute a well established class of games in model checking and verification. In connectivity games, the objective of one of the players is to visit every node of the game graph infinitely often. The first contribution of this paper is our proof that solving connectivity games can be reduced to the incremental strongly connected component maintenance (ISCCM) problem, an important problem in graph algorithms and data structures. The second contribution is that we non-trivially adapt two known algorithms for the ISCCM problem to provide two efficient algorithms that solve the connectivity games problem. Finally, based on the techniques developed, we recast Horn's polynomial time algorithm that solves explicitly given Müller games and provide an alternative proof of its correctness. Our algorithms are more efficient than that of Horn's algorithm. Our solution for connectivity games is used as a subroutine in the algorithm.

Connectivity in the presence of an opponent

TL;DR

This work studies connectivity in Müller games by reducing connectivity solving to incremental SCC maintenance (ISCCM) through a derivative sequence, enabling two efficient ISCCM-based algorithms with parameterized runtimes that outperform naive bounds. It also delivers a rigorous, self-contained correctness proof for Horn's polynomial-time algorithm for explicitly given Müller games, showing how the connectivity subroutine underpins the broader solver. The two algorithms achieve favorable time complexities in sparse and dense regimes and, when combined with Horn-like reductions, substantially improve practical solvability of Müller games in model checking. Overall, the paper advances both theoretical understanding and algorithmic practicality for solving connectivity and Müller games, with direct implications for verification and synthesis pipelines.

Abstract

The paper introduces two player connectivity games played on finite bipartite graphs. Algorithms that solve these connectivity games can be used as subroutines for solving Müller games. Müller games constitute a well established class of games in model checking and verification. In connectivity games, the objective of one of the players is to visit every node of the game graph infinitely often. The first contribution of this paper is our proof that solving connectivity games can be reduced to the incremental strongly connected component maintenance (ISCCM) problem, an important problem in graph algorithms and data structures. The second contribution is that we non-trivially adapt two known algorithms for the ISCCM problem to provide two efficient algorithms that solve the connectivity games problem. Finally, based on the techniques developed, we recast Horn's polynomial time algorithm that solves explicitly given Müller games and provide an alternative proof of its correctness. Our algorithms are more efficient than that of Horn's algorithm. Our solution for connectivity games is used as a subroutine in the algorithm.
Paper Structure (18 sections, 31 theorems, 9 equations, 9 figures)

This paper contains 18 sections, 31 theorems, 9 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Müller games given explicitly
  3. Connectivity games
  4. Our contributions
  5. A characterization theorem
  6. Solving connectivity games efficiently
  7. Efficiency results
  8. Revisiting the ISCCM problem
  9. General frameworks
  10. The first framework
  11. The second framework
  12. Proofs of Theorem \ref{['Thm:|V_0|']} and Theorem \ref{['Thm:|V_1|']}
  13. The ISCCM$(m,k)$ algorithm
  14. Explicitly given Müller games
  15. Full proof of Horn's algorithm
  16. ...and 3 more sections

Key Result

Lemma 1

Let $\mathcal{C}=\{C_1,C_2,\ldots,C_k\}$, where $k>1$, be a collection of FTs that partition the game graph $G$. If $\mathcal{G}$ is forced-connected then for every $X\in \mathcal{C}$ there is a distinct $Y\in \mathcal{C}$ such that either $Y$ is a singleton consisting of a player 1's node and $E(Y)

Figures (9)

  • Figure 1: Implementation of DFCG-M-K function
  • Figure 2: Implementation of UPDATE-INDEGREE function
  • Figure 3: Implementation of DFCG function
  • Figure 4: Algorithm for explicit Müller games
  • Figure 5: The counter case of Lemma 6,7 in Horn's paper
  • ...and 4 more figures

Theorems & Definitions (56)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • ...and 46 more