Graduate Seminar: Anton Pirogov: Automata-theoretic techniques for probabilistic verification

Thursday, February 18, 2021, 10:00am

Anton Pirogov: Automata-theoretic techniques for probabilistic verification


Büchi automata can be seen as a straight-forward generalization of ordinary NFA, adapted to handle infinite words. While they were originally introduced for applications in decidability of logics, they became a popular tool for practical applications, e.g. in automata-based approaches to model checking and synthesis problems. Being arguably both the simplest and most well-known variant in the zoo of so-called omega-automata that are considered in this setting, they serve as an intermediate representation of omega-regular specifications of verification or synthesis requirements that are usually expressed in a more declarative fashion, e.g. using linear temporal logic.

Unfortunately, nondeterministic automata are not directly suitable for certain applications, whereas deterministic Büchi automata are less expressive. This problem is usually solved by either constructing deterministic automata of a different kind, or by restricting their ambiguity, i.e., the maximal number of accepting runs on some word. In both cases, the transformation is expensive, yielding an exponential blow-up of the state space in the worst case. 
optimized constructions and heuristics for common special cases are useful and in demand for actual practical applications.

In this talk we present a new general construction for determinization from nondeterministic Büchi to deterministic parity automata that unifies the dominant branches of previous approaches based on the Safra construction and the Muller-Schupp construction. Additionally, we sketch a number of new heuristics for determinization, some of which exploit properties of our unified construction.

Apart from the classical nondeterministic and deterministic variants of automata, it is natural to consider probabilistic automata, i.e., automata that use a probability distribution on the states instead of nondeterminism to decide which state to go to next. It is known that in general, such automata are more expressive than classical automata and many decision problems are undecidable.
We present subclasses of probabilistic automata that correspond to certain ambiguity classes and are not more expressive than classical automata.

Thursday, 18.02.2021, 10:15 am
online as Zoom-Videocall:
Meeting-ID: 965 1955 6069
Kenncode:   482378