| Summary: | 博士 === 國立臺灣大學 === 資訊管理學研究所 === 101 === The automata-theoretic approach to model checking has been developed for near three decades. Because of its proven effectiveness and ease of use, the approach has become a viable alternative to testing and simulation in industry. In the approach, a system is typically represented by a Buchi automaton, while a specification is encoded by a formula in propositional linear temporal logic (PTL), of which the future fragment (usually referred to as LTL) is more often used. The approach proceeds by translating the negation of the formula to a Buchi automaton, which is later intersected with the system automaton for testing emptiness. Such translation plays an important role in the approach because in general, the smaller the negated-specification automaton is, the sooner the model checking process may be completed. Although there has been a long line of research on LTL translation algorithms aiming to produce smaller automata, there are still opportunities of improving translation algorithms for other temporal logics such as PTL, which is expressively more succinct than LTL.
Specifications may also be directly encoded by Buchi automata which in certain cases are more natural and easier than temporal formulae. In such cases, complementation of a specification automaton is performed before taking the intersection with the system automaton. The complementation of Buchi automata is significantly more complicated than that of classic finite automata on finite words. Optimization heuristics are critical to good performance. Due to the high complexity of Buchi complementation, much recent emphasis has been shifted to containment testing without constructing the complement. The Ramsey-based approach has been proven to be quite effective in such containment testing, although it is not competitive in complementation where the determinization-based approach is the best in general. Again, to expedite the model checking process, we can improve not only the translation algorithm but also the complementation algorithm and the containment testing algorithm.
For translation of temporal formulae, we extend five existing incremental algorithms with a backtrace procedure to support past operators of PTL, while maintaining the advantages of incremental automata construction. The cover computation common to the state-based incremental algorithms is improved based on prime implicants to obtain smaller automata. Besides, we also implement the separation of past and future separators. The separation procedure can convert a PTL formula to an equivalent LTL formula, which can later be translated by an efficient LTL translation algorithm such as LTL2BA or LTL3BA. This allows us to compare our extended algorithms with those existing efficient LTL translation algorithms.
For Buchi complementation, we review four approaches and perform a comparative experimentation on the best construction in each approach. Although the conventional wisdom is that the nondeterministic approaches are better than the deterministic approach because of better worse-case bounds, our experimental results show that the deterministic construction is the best for complementation in general. We also propose optimization heuristics for three of the four best constructions. Our experiment shows that the optimization heuristics substantially improve the three constructions.
For containment testing, we propose an incremental containment testing approach based on the determinization-based constructions, of which Safra-Piterman construction is the best in Buchi complementation. Although the determinization-based constructions are typically performed in stages, we show that the stages can be merged such that the containment testing can be performed incrementally. Our experimental results show that for cases where the containment relation holds, our incremental Safra-Piterman approach is much better then the Ramsey-based approach. For other cases where the containment relation does not hold, the Ramsey-based outperforms our incremental Safra-Piterman approach.
Finally, we address the issue of tool support for education and research on ω-automata and temporal logics. Although there are various tools for automata-theoretic model checking, none of the tools provide facilities for visually manipulating automata and temporal formulae. This motivated our GOAL tool, which is the first interactive graphical tool for learning ω-automata and temporal logics. Besides, GOAL also provides facilities for helping researchers develop and test new algorithms, perform experiments, and collect statistical data. We also build a Web-based tool called Buchi Store, which is an extensible collection of temporal formulae and their equivalent automata. Such a collection can be used not only as a new translation tool that always returns the smallest automata available but also as benchmark cases for experiments. Both GOAL and Buchi Store already helped us develop our improved algorithms, which expedite the model checking process. We believe the two tools provide researchers with a good environement for future development and experimentation of related algorithms.
|
|---|
