基於自動機理論的模型檢測演算法與工具之改善

Improved Algorithms and Tools for Automata-Theoretic Model Checking

蔡明憲(Ming-Hsien Tsai)

指導教授 ： 蔡益坤

共同指導教授 ： 王柏堯(Bow-Yaw Wang)

國立臺灣大學/管理學院/資訊管理學研究所/博士(2013年)

https://doi.org/10.6342/NTU.2013.02165

摘要

以自動機理論為基礎的模型檢測方法已經發展近三十年，此方法被認為具有效率且容易使用，在確保軟體或硬體設計的正確性上，已成為業界測試與模擬之外的另一項選擇。在這個方法中，一個待測的系統會用一個Buchi自動機來表示，而系統所需滿足的規格則用一個線性時態邏輯（PTL）式來表示。在線性時態邏輯中，比較常用到的是只能描述未來的版本（LTL）。此方法首先將規格的否定轉換成一個Buchi自動機，然後和表示系統的自動機作交集，最後測試交集部分是否不接受任何行為。在這些步驟中，時態邏輯式的轉換扮演一個重要的角色，因為一般來說，轉換出來的自動機越小，則與系統的交集也越小，而模型檢測可以比較快完成。雖然目前已經有很多LTL轉換演算法，然而在其他時態邏輯的部分，仍有改善的空間，例如比LTL更容易書寫較短規格的PTL。

系統規格也可以直接用Buchi自動機來表示，在某些情況下會比時態邏輯式更自然與直接。如此一來，在與系統自動機作交集之前，需要先計算規格自動機的補集。Buchi自動機的補集計算與有限字串長度的傳統自動機相比更加複雜許多，所以一些最佳化方法對補集計算的效能與效率有很大的幫助。因為Buchi自動機補集的高複雜度，最近許多研究都跳往不需完整建置補集的漸進式行為包含測試。在行為包含測試中，以Ramsey理論為基礎的方法已被證明相當有效率，不過在補集計算的部分卻相當不具競爭力，反而確定性方法是最好的。同樣地，為了加速模型檢測，我們除了改進時態邏輯轉換演算法之外，也可以改進補集計算與包含測試的演算法。

在時態邏輯轉換的部分，我們改善了五個漸進式演算法，利用一個回朔的程序讓這些演算法可以支援過去時態運算子，同時保持漸進式轉換的好處。對於狀態基礎演算法中的涵蓋計算程序，我們也利用質含項（Prime Implicant）加以改善。此外，我們也實作了過去與未來的分離程序，使得一個PTL式子可以被轉換成另一個相等的LTL式子，然後再利用目前最有效率的LTL轉換演算法（例如LTL2BA或是LTL3BA）來轉換。這使得我們可以比較我們所改善的演算法，以及目前最有效率的LTL轉換演算法。

在Buchi補集計算的部分，我們審視四個主要方法，並透過實驗加以比較。雖然傳統的看法是非確定性方法比確定性方法更好，因為非確定性方法有比較低的理論複雜度。然而我們的實驗顯示在Buchi補集計算中，確定性方法是最好的。此外，我們也對其中三個方法提出數個改善的點子，使得這三個方法的效率與效能大為改善。

在包含測試中，我們提出一個基於確定性方法的漸進式包含測試演算法。雖然確定性方法的執行一般被認為需要分離成幾個階段，不過我們展示這些階段其實可以合併成一個，而且可以被漸進式地執行。實驗顯示包含關係成立時，我們的方法比以Ramsey理論為基礎的方法來得好。不過包含關係不成立時，以Ramsey理論為基礎的方法卻比我們的方法來得好。

最後，我們要應付的問題是自動機與時態邏輯在教育與研究的工具支援。雖然目前已有許多以自動機理論為基礎的模型檢測工具，不過都沒有支援自動機或時態邏輯式視覺化呈現與操作。這激發了我們的第一個工具：GOAL，第一個可以用來學習無限自動機與時態邏輯的視覺化互動工具。除此之外，GOAL也提供功能幫助研究學者開發和測試新演算法、執行實驗、與收集統計資料。除了GOAL以外，我們還建制一個網頁形式的工具：Buchi Store。這個工具是許多常見時態邏輯式與其最小相等自動機的集合，可以被搜尋、瀏覽與擴展。這樣的集合不僅可以當成一個最佳時態邏輯式轉換演算法，同時也可以作為實驗的比較基礎。GOAL與Buchi Store已經幫助我們開發許多改進的演算法，讓模型檢測更加快速。我們相信這兩個工具可以提供研究學者一個好的平台，幫助未來開發相關演算法與進行實驗。

關鍵字

自動機 ； 模型檢測 ； 時態邏輯

並列摘要

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.

並列關鍵字

Automata ； Model Checking ； Temporal Logic

參考文獻

[1] P. Abdulla, Y.-F. Chen, L. Clemente, L. Hol ́ık, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation subsumption in Ramsey-based Buchi automata universality and inclusion testing. In CAV 2010, LNCS 6174, pages 132–147. Springer, 2010.

[4] C. Altho↵, W. Thomas, and N. Wallmeier. Observations on determinization of Buchi automata. TCS, 363(2):224–233, 2006.

[5] A. Ben-Amram and C. Lee. Program termination analysis in polynomial time. TOPLAS, 29(1), 2007.

[7] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE TC, 35(8):677–691, 1986.

[8] J. Buchi. On a decision method in restricted second order arithmetic. In ICLMPS 1960, pages 1–12. Stanford University Press, 1962.