Automata-Theoretic Techniques in Probabilistic Verification
Probabilistic verification is concerned with questions as obtaining the probability for the satisfaction of certain correctness properties with respect to the behaviour of software systems. Such properties are represented in a suitable formalism (like Linear Temporal Logic (LTL)) and are verified on some abstraction (e.g. Markov chain) of the system of interest that preserves the properties in question. Linear Temporal Logic was proposed by Pnueli as a suitable language for specifications and can express many classes of useful properties (Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46‑57). A useful property of LTL is that every LTL formula can be translated into omega-automata.
Omega-automata are finite-state automata that read infinite words, which turn out to be an adequate representation of traces of program executions, which in the case of reactive, non-terminating systems are infinite. The set of possible program executions can be seen as a language of infinite words and a correctness property can be seen as a description of the set of program traces that are admissible, i.e. do not violate the property. From the logical, descriptive formulation in e.g. LTL one can obtain an operational representation as a corresponding omega-automaton that accepts all words that satisfy the property and rejects the others. This allows for the reduction of verification problems to problems based on the graphs that underlie the automata and the abstraction of the system. Automata-based techniques have proven to be a successful approach for solving verification problems due to the existence of algorithmic solutions that are also feasible in practice, hence this is often the approach of choice for tackling verification tasks in various settings.
Multiple acceptance mechanisms, most of which are equivalent in expressivity, are known for omega-automata. While in classical model checking a nondeterministic automaton suffices, in the probabilistic setting restrictions on the nondeterminism are necessary and the classical solution is first to obtain a nondeterministic automaton from the specification and then performing a complete determinisation of the automaton in the next step. The omega-automata obtained in the first step are usually Büchi-automata, i.e. use the Büchi acceptance condition (Büchi, J. Richard. "On a Decision Method in Restricted Second Order Arithmetic." Studies in Logic and the Foundations of Mathematics. Vol. 44. Elsevier, 1966. 1-11) by which a word (i.e. program trace) is accepted if there exists an execution of the automaton that visits final states infinitely often. But as such automata are strictly less expressive under determinism, more powerful acceptance mechanisms must be used in the resulting automaton.
A breakthrough result by Safra (Safra, Shmuel. "On the complexity of omega-automata." Foundations of Computer Science, 1988., 29th Annual Symposium on Foundations of Computer Science. IEEE, 1988) provided the first asymptotically optimal translation from nondeterministic Büchi to deterministic Rabin automata (which use a different definition of acceptance) and today a number of different translations with the same asymptotic bound are known. But the optimality applies only to the worst-case, while in practice often much smaller deterministic automata can be constructed. Hence, in practice, there is much room for heuristic approaches that produce small automata for specific kinds of inputs and in special cases the rather complex construction by Safra can even be avoided.
This dissertation project is concerned with the improvement of automata-based techniques in the context of probabilistic verification. The first goal is the improvement of determinisation of omega-automata by development of new algorithms and heuristics that ideally should work well (i.e. produce small automata) on many practically relevant classes of inputs. The second goal is research into other known or novel automata models (and suitable restrictions of those) which can be applied for probabilistic model-checking by adapting existing or developing new techniques for this purpose. The size of the used automata, depending both on the automaton model and the algorithms that produce them, is critical for the feasibility of verification tasks, due to usually limited computational resources. Hence, results of this project will directly benefit the application of verification techniques in practice.