Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.07548 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929225942958080 |
|---|---|
| author | Majumdar, Rupak Saglam, Irmak Thejaswini, K. S. |
| author_facet | Majumdar, Rupak Saglam, Irmak Thejaswini, K. S. |
| contents | We provide an algorithm to solve Rabin and Streett games over graphs with $n$ vertices, $m$ edges, and $k$ colours that runs in $\tilde{O}\left(mn(k!)^{1+o(1)} \right)$ time and $O(nk\log k \log n)$ space, where $\tilde{O}$ 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\left(mn^2(k!)^{2+o(1)}\right)$, 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 \emph{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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_07548 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Rabin Games and Colourful Universal Trees Majumdar, Rupak Saglam, Irmak Thejaswini, K. S. Logic in Computer Science Data Structures and Algorithms Formal Languages and Automata Theory F.4.1; G.2.1 We provide an algorithm to solve Rabin and Streett games over graphs with $n$ vertices, $m$ edges, and $k$ colours that runs in $\tilde{O}\left(mn(k!)^{1+o(1)} \right)$ time and $O(nk\log k \log n)$ space, where $\tilde{O}$ 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\left(mn^2(k!)^{2+o(1)}\right)$, 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 \emph{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. |
| title | Rabin Games and Colourful Universal Trees |
| topic | Logic in Computer Science Data Structures and Algorithms Formal Languages and Automata Theory F.4.1; G.2.1 |
| url | https://arxiv.org/abs/2401.07548 |