An optimal automata approach to LTL model checking of probabilistic systems

Most verification problems on finite systems may be formulated and solved optimally using automata based techniques. Nonetheless LTL verification of (finite) probabilistic systems, i.e. deciding whether a probabilistic system almost surely satisfies an LTL formula, remains one of the few exceptions to this rule. As a matter of fact, existing automata-based solutions to this problem lead to double EXPTIME algorithms, while Courcoubetis and Yannakakis provide an optimal one in single EXPTIME. In this study, we remedy this exception. Our optimal automata based method proceeds in two steps: we present a minimal translation from LTL to omega-automata and point out appropriate properties on these automata; we then show that checking whether a probabilistic system satisfies an omega-automaton with positive probability can be solved in linear time for this kind of automata. Moreover we extend our study to the evaluation of this probability. Finally, we discuss some experimentations with our implementation of these techniques: the ProbaTaf tool.