時間邏輯至自動機轉譯演算法之比較研究

Abstract

Buchi 自動機與線性時間邏輯是模型檢驗的自動機理論方法中的兩項根本元件，Buchi 自動機常用於表示系統的模型，而命題線性時間邏輯則用於表示系統模型中想要符合的性質，這個自動機理論模型檢驗方法包含了把一個用命題線性時間邏輯描述的否定規格轉譯成一個 Buchi 自動機，而這個 Buchi 自動機會跟表示系統模型的自動機做交集，並檢查是否為空集，原則上，轉譯而成的 Buchi 自動機愈小，模型檢驗的程序也就愈快。多年來，有很多的命題線性時間邏輯至 Buchi 自動機的轉譯演算法被發展出來，這些演算法使用不同的中間結構，而且對於一個公式，不同演算法所轉譯出來的 Buchi 自動機大小都不太相同，雖然已經有很多比較其中一些演算法的成果，但是他們在於演算法的數量或是命題線性時間邏輯公式的型態不夠完整，這個論文的目標就是要提供一個較完整的比較以及解釋這些演算法中的不同。 在這篇論文中，我們比較了六個著名的轉譯演算法，這些比較包含了使用不同的最佳化技巧的組合於轉譯的 Buchi 自動機上。在這些我們所考慮的演算法中，尤其是幾個 on-the-fly 的演算法不適用於包含過去運算子的公式，為了使得這些比較完整以及公平，我們延伸了這些 on-the-fly 的演算法，使得他們能支援過去運算子，並且同時保持了遞增 tableau 建造的優點，這個延伸到目前似乎是新的。我們希望這樣的一個比較性研究可以幫助其他的研究者於選擇適當的轉譯演算法以及獲得那些最小的可能 Buchi 自動機，而這個研究的副產物就是我們延伸實做了五個轉譯演算法於一個名為 GOAL 的自動機與時間邏輯的圖形化輔助學習工具，這個工具的前一版本只有六個演算法中的一個並使用 tableau 建造方法，這個工具現在不只達到了教育目的，而且提供了一個命題線性時間邏輯至 Buchi 自動機轉譯演算法之比較研究的平台。

Buchi automata and linear temporal logic are fundamental components of the automata-theoretic approach to model checking, where Buchi automata are used to represent systems, while Propositional Linear Temporal Logic (PTL) is used to specify properties of a system. The approach involves translation of a negated specification PTL formula into a Buchi automaton, which is then intersected with the system automaton and checked for emptiness. In principle, the smaller the translated Buchi automaton, the faster the model checking process. Over the years, numerous algorithms for PTL to Buchi automata translation have been developed. These algorithms construct automata using different intermediate structures and, for a given PTL formula, generate automata of different sizes. Although there have been works comparing some of these algorithms, they are not quite complete in the number of algorithms or in the types of PTL formulae. The goal of this thesis is to provide a more complete comparison and to explain some of the differences between these algorithms. In this thesis, we compare six well-known translation algorithms. Comparisons are made with various combinations of optimization techniques being applied to the translated Buchi automaton. Some of the translation algorithms considered, in particular several on-the-fly algorithms, do not apply for formulae containing past operators. To make the comparisons complete and fair, we extend these on-the-fly algorithms to support past operators, while maintaining the advantages of incremental temporal tableau construction. The extension seems to be new. We hope that such a comparative study would help other researchers in choosing the appropriate translation algorithm and obtaining the smallest possible translated Buchi automaton. As a by-product of this research, we extend the GOAL tool, a graphical tool for manipulating omega-automata and temporal formulae, with five of the six translation algorithms. The previous version of GOAL had only one of the six translation algorithms using tableau construction. The GOAL tool now not only serves educational purposes but also provides a platform for comparative studies of PTL to Buchi automata translation algorithms.