[FM-India]IARCS Verification Seminar Series -- Talk by Soumyajit Paul on Sept. 16 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Soumyajit Paul, a post-doctoral researcher at the University of Liverpool. The talk is scheduled on Tuesday, September 16, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=M2EzajE4cThqcG9lY2VyaXZndXNiajNhN2MgdnNzLmlhcmNzQG0&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, Organizers, IARCS Verification Seminar Series ============================================================= Title: Resolving Nondeterminism by Chance Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. The notion of History Determinism (sometimes known as Good for Games) was introduced by Henzinger and Piterman in 2006 motivated by applications in reactive synthesis. Later, it has been studied for several models such as Pushdown systems, Timed automata, Vector Addition systems, etc. Motivated by checking qualitative properties in probabilistic verification, we introduce the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. In this talk, I will present our work on stochastic resolution of nondeterministic automata. I will discuss the expressiveness of stochastically-resolvable automata as well as our complexity results for deciding stochastic resolvability. In particular, we show that it is undecidable to check if a given NFA is stochastically resolvable with a given threshold. The problem however becomes decidable for the class of finitely-ambiguous automata. We also consider the related question of deciding whether an automata is resolvable with any positive threshold. We show that this problem is decidable for automata over unary alphabet as well as for finitely-ambiguous automata. I will present our complexity results for several well-studied classes of automata and also discuss natural extensions of some of these results to automata for omega regular languages. I will conclude with some interesting open questions. This is based on joint work with David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke and Di-de Yen. Bio: Soumyajit Paul is currently a post-doctoral researcher at University of Liverpool, working primarily with Sven Schewe. His research interests encompasses algorithmic game theory, probabilistic systems and formal methods. Earlier, he was a teaching and research fellow at Université Paris Cité, affiliated to IRIF. He did his PhD at LaBRI, Université de Bordeaux under the supervision of Hugo Gimbert and B. Srivathsan. His PhD research work focussed on the complexity of equilibrium computations in games where players may have imperfect information. Prior to his PhD, he completed his undergraduate and master's studies at Chennai Mathematical Institute.