Title: Solving Rabin games using Colourful Universal Trees

Speaker: Thejaswini Raghavan    (bio) (bio)

Thejaswini Raghavan is a postdoctoral researcher at IST Austria in the group headed by Thomas A. Henzinger. She did her Ph.D. under the supervision of Marcin Jurdzinski at the University of Warwick. Prior to that, she did her B.Sc. (Hons.) in Mathematics and Computer Science and M.Sc. in Computer Science from Chennai Mathematical Institute (CMI). Her research interests broadly lie in Logic, Automata, Games, and Verification.

When: Tuesday, 23 January 2024 at 1900 hrs (IST)       

Abstract:
To solve Church's synthesis problem for omega-regular specifications, represented by non-deterministic Buechi automata, there are two polynomial-time equivalent approaches: either reduce it to the emptiness problem for Rabin tree automata or solve a Rabin game.

In this talk, we will see how one can solve Rabin games faster with an improvement by a super quadratic dependence on the number of Rabin pairs from the currently best known run time 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 Jurdzinski and Lazic (2017) to solve parity games, as well as of Rabin progress measures of Klarlund and Kozen (1991). Further, we will also discuss lower bounds for solving Rabin games that show that our algorithm is tight subject to the exponential time hypothesis, reproving a result of Calude et al. (2022).

The first part of the talk is based on joint work with Rupak Majumdar and Irmak Saglam, accepted at TACAS 2024 and the last part about the lower bounds is based on joint work with Antonio Casares, Marcin Pilipczuk, Michal Pilipczuk, Ueverton S. Souza, published at SOSA 2024.