17 Jan
2024
17 Jan
'24
1:12 p.m.
Dear all,
The next talk in the IARCS Verification Seminar Series will be given
by Thejaswini Raghavan, a postdoctoral researcher at IST Austria. The talk
is scheduled on Tuesday, Jan. 23, at 1900 hrs IST (add to Google calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MjQxam5sb2ZjaGFlanV1a3RzOGliZzhocmQgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com>
).
The details of the talk can be found on our webpage (
https://fmindia.cmi.ac.in/vss/), and also appended to the body of this
email.
The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.
All are welcome to join.
Best regards,
Akash, Deepak, Madhukar, Srivathsan
=============================================================
Title: Solving Rabin games using Colourful Universal Trees
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)
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.
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.