自動機與時態邏輯的圖形化輔助學習工具

Abstract

在用於模型檢驗的自動機理論方法中，omega自動機和時態邏輯是兩項基本元件。omega自動機，尤其是 Büchi 自動機，常用於表示系統的模型； 而時態邏輯，特別是命題線性時態邏輯 (PTL)，則用於表示系統模型中想要符合的性質。在這個自動機理論的模型檢驗的方法中，ㄧ項重要的步驟是藉由tableau或其他的轉換方法把PTL式子轉換成 Büchi 自動機。因為轉換過程的複雜性，使得PTL式子和 Büchi 自動機之間的關聯性不容易理解。除了PTL到 Büchi 自動機的轉換過程外，在學習自動機的ㄧ些特性和操作時，也可能遭遇困難，特別是在互補的操作上。所以通常是藉由演算一些例子的來了解PTL的轉換和互補的演算法。但由於演算法過程的繁複性，正確無誤的徒手計算並非特別情況的例子是不容易的。因此，一個可以處理omega自動機和時態邏輯且具有互動性的圖形化工具，對於學習這些演算法應該會有所助益。 在這篇論文中，我們設計並實作了ㄧ個如上述所說的圖形化工具，工具的名稱是GOAL。雖然GOAL的最終目標是提供支援各種omega自動機和一般化的線性時態邏輯的學習工具，但是在目前的版中，GOAL只專注於命題線性時態邏輯(PTL)和Büchi 自動機開發。使用者藉由GOAL可以做到如下的事情：ㄧ步ㄧ步的轉換含有過去運算子的PTL式子到Büchi 自動機、取兩個Büchi 或是兩個一般化Büchi 自動機的聯集或交集、取Büchi 自動機的互補形式、檢驗Büchi 和一般化Büchi 自動機所接受的語言是否為空集合、檢驗兩個Büchi 自動機所接受的語言是否相等或是否有包含關係、在使用者所建立的Büchi 自動機和一般化Büchi 自動機上做字串的模擬輸入測試、化簡一般化Büchi 自動機的大小、檢驗Büchi 自動機是否有模擬的相等關係、在一般化Büchi 自動機和Büchi 自動機之間作轉換。我們相信，在具有互動性的圖形化工具輔助下，使用者將可以更容易的學習omega自動機和時態邏輯。

Omega-automata and temporal logic are two fundamental components in the automata-theoretic approach to model checking. Omega-automata, in particular B¨uchi automata, are often used as system models, while temporal logic, in particular propositional linear temporal logic (PTL), is used to specify the desired properties of a system. In this approach to model checking, one critical step is to translate PTL formulae into B¨uchi automata by using tableau or other methods. Because the translation process is complex, the correspondence between a PTL formula and its equivalent B¨uchi automaton is not easy to comprehend. Besides the PTL formulae to B¨uchi automata translation, one may also have difficulty in learning some automata properties and operations, in particular complementation. To understand a PTL translation algorithm or a complementation algorithm, one typically tries out a few examples. Due to the tedious procedures, it is not easy for one to work out nontrivial examples correctly with all the details by using pencil and paper. Therefore, an interactive graphical tool that can handle omega-automata and temporal logic should be useful. In this thesis, we design and implement such an interactive graphical tool, named GOAL. Although our eventual goal is for the GOAL tool to support most variants of omega-automata and linear temporal logic, the current version of GOAL focuses on PTL and B¨uchi automata. With GOAL, the user can translate a PTL formula allowing past operators into a B¨uchi automaton step by step, take the union and intersection of two B¨uchi automata, complement a B¨uchi automaton, check emptiness of B¨uchi and generalized B¨uchi automata, check language containment and equivalence for B¨uchi automata, test runs on user-specified B¨uchi automata and generalized B¨uchi automata, reduce the size of a generalized B¨uchi automaton, check simulation equivalence of B¨uchi automata, and perform transformations between generalized B¨uch automata and B¨uchi automata. We believe that, by using an interactive graphical tool, the user can learn omega-automata and temporal logic more easily.