Verification algorithms based on alternating automata.

摘要

This thesis presents a collection of algorithms for the automated verification of reactive systems based on alternating o-automata. We consider three different verification problems. Dynamic verification proves the correctness of program traces collected at run-time. Trace evaluation additionally collects data over such traces. Static verification proves the correctness of the system design by showing that all possible traces are correct.; The standard constructions for these verification problems are based on nondeterministic automata. Nondeterministic automata have simple decision algorithms, but they suffer from the state explosion problem: the size of the nondeterministic automaton increases exponentially when multiple components are combined into a single automaton and when the language of an automaton is complemented. We present new solutions based on alternating automata. Since alternating automata provide a linear representation, this approach can save an exponential amount of space compared to nondeterministic automata.; For dynamic verification, we propose three different algorithms, with different performance characteristics. All three are based on a traversal of the alternating automaton, but apply different traversal strategies. For trace evaluation, we introduce algebraic alternating automata, an extension that associates a value with each run of the automaton. We show how statistical queries can be translated into algebraic alternating automata. For static verification, we propose an incremental solution that first checks for safety violations, and then verifies different types of liveness properties.; We also study two approaches for the efficient implementation of the verification algorithms. The symbolic methods replace the explicit manipulation of states by operations on symbolic representations of sets of states and sets of sets of states. The state space reduction technique merges equivalent nodes to reduce the size of the alternating automaton.