Rabin Games and Colourful Universal Trees
CoRR(2024)
摘要
We provide an algorithm to solve Rabin and Streett games over graphs with n
vertices, m edges, and k colours that runs in
Õ(mn(k!)^1+o(1)) time and O(nklog k log n) space,
where Õ hides poly-logarithmic factors. Our algorithm is an
improvement by a super quadratic dependence on k! from the currently best
known run time of O(mn^2(k!)^2+o(1)), obtained by converting a
Rabin game into a parity game, while simultaneously improving its exponential
space requirement.
Our main technical ingredient is a characterisation of progress measures for
Rabin games using colourful trees and a combinatorial construction of
succinctly-represented, universal colourful trees. Colourful universal trees
are generalisations of universal trees used by Jurdziński and Lazić
(2017) to solve parity games, as well as of Rabin progress measures of Klarlund
and Kozen (1991). Our algorithm for Rabin games is a progress measure lifting
algorithm where the lifting is performed on succinct, colourful, universal
trees.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要