Abstract

History-deterministic (HD) 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 has an accepting run, then the constructed run is also accepting. These automata have found important applications in reactive synthesis. In this talk I will discuss our work on a generalisation of HD automata called stochastically resolvable automata : the strategy for resolving non-determinism may randomise, and the input word only needs to be accepted with some threshold probability.

Not all NFAs are stochastically resolvable and a key challenge is to recognise such automata. It turns out 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. For the general question of stochastically resolving an automaton with any arbitrary positive threshold, the problem is decidable for automata over a unary alphabet, as well as for finitely-ambiguous automata. 

I will also discuss natural extensions of this concept to automata over infinite words and touch on some applications. I will conclude with several interesting open questions on this topic.

links:

• label: Meeting url: https://teams.microsoft.com/meet/3672057999870?p=MUiWeMo4Y5yPx5mz8g icon: fa-solid fa-video featured: true