Verification Series

Resolving Nondeterminism by Chance

16th October 2025, 11:00 add to calenderAshton 208
Soumyajit Paul
Liverpool

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 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
add to calender (including abstract)

Additional Materials