Connectivity in the presence of an opponent

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Liang, Zihui, Khoussainov, Bakh, Takisaka, Toru, Xiao, Mingyu
Format: Preprint
Publié: 2023
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866913649920049152
author Liang, Zihui
Khoussainov, Bakh
Takisaka, Toru
Xiao, Mingyu
author_facet Liang, Zihui
Khoussainov, Bakh
Takisaka, Toru
Xiao, Mingyu
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2304_08783
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle Connectivity in the presence of an opponent
Liang, Zihui
Khoussainov, Bakh
Takisaka, Toru
Xiao, Mingyu
Computer Science and Game Theory
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.
title Connectivity in the presence of an opponent
topic Computer Science and Game Theory
url https://arxiv.org/abs/2304.08783