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

• Main Authors: Kang-Nien Wu, 吳康年
• Other Authors: Yih-Kuen Tsay
• Format: Others
• Language: en_US
• Published: 2005
• Online Access: http://ndltd.ncl.edu.tw/handle/32625121645194205132

碩士 === 國立臺灣大學 === 資訊管理學研究所 === 95 === 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.