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

GOAL: A Graphical Tool for Learning Omega-Automata and Temporal Logic

吳康年(Kang-Nien Wu)

指導教授 ： 蔡益坤

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

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

摘要

在用於模型檢驗的自動機理論方法中，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自動機 ； Buchi 自動機 ； 時態邏輯 ； PTL ； 圖形化工具 ； 驗證 ； 模型檢驗

並列摘要

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.

並列關鍵字

Automata Theory ； Omega-automata ； Buchi Automata ； Temporal Logic ； PTL ； Graphical Tool ； Verification ； Model Checking

參考文獻

[4] J. R. Buchi. On a decision method in restricted second order arithmetic. In Proceeding of the International Congress on Logic, Methodology and Philosophy of Science, pages 1–12, 1960.

[5] J. R. Buchi. Decidable theories ii-the monadic second-order theory of omega-1. pages 1–128, 1973.

[6] Y. Choueka. Theories of automata on omega-tapes: A simplified approach. Journal of Computer and System Science, 8:117–141, 1974.

[7] Edmund M. Clarke and I. Draghicescu. Expressibility results for linear time and branching time logics.

[8] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, pages 52–71, 1981.