Probabilistic automata and verification

Christel Baier, Technische Universitaet Dresden Automata-based model checking relies on a representation of the system and the properties to be verified by finite-state automata. In the classical setting, nondeterministic automata are used for both the system and the properties, and verification amounts analyzing the product of these two nondeterministic automata by means of graph algorithms. In this talk, we address the automata-based approach for verifying randomized systems modeled by some kind of probabilistic automata. Technical problems in the definition of the product arise when dealing with nondeterministic automata for the property to be verified. One solution is to switch to deterministic automata for the requirements, but this can cause a double exponential blow-up for the construction of an automata for a given logical formula (e.g., LTL) formalizing the requirements. An alternative obvious idea is the use of a probabilistic automata representing the properties. This, however, leads to the undecidability of the verification problem. Nevertheless there are some special instances of the verification problem that can be solved algorithmically in an elegant way using probabilistic automata for both the system and the property.