GOAL: A Graphical Tool for Learning Omega-Automata and Temporal Logic
Date Issued
2006
Date
2006
Author(s)
Wu, Kang-Nien
DOI
en-US
Abstract
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.
Subjects
自動機理論
omega自動機
Buchi 自動機
時態邏輯
PTL
圖形化工具
驗證
模型檢驗
Automata Theory
Omega-automata
Buchi Automata
Temporal Logic
Graphical Tool
Verification
Model Checking
Type
other
File(s)![Thumbnail Image]()
Loading...
Name
ntu-95-R93725024-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):259d6ea8aea725343869ca8fc5995105