Title: Resolving Nondeterminism by Chance

Speaker: Soumyajit Paul    (bio) (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.

When: Tuesday, 16 September 2025 at 1900 hrs (IST)       

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.