Verification Series
2025-10-16 11:00 - 12:00 | Ashton 208
Soumyajit Paul: Resolving Nondeterminism by Chance

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 Peterman 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 study 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

https://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1292
