時序性質之轉換、分類及其應用

Transformation and Classification of Temporal Properties with Applications

常怡文(Yi-Wen Chang)

指導教授 ： 蔡益坤

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

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

摘要

無資料

關鍵字

Buchi自動機 ； Buchi Store ； 分類 ； GOAL ； Omega自動機 ； 時序邏輯 ； 轉換 ； 程試驗證

並列摘要

In the automata-based approach, the model checking problem can be stated as follows: given a system M and a temporal property f, determine whether the intersection of A_M and A_~f is empty, where A_M is a Buchi automaton representing the system M and A_~f is an automaton representing the negation of the given property f. In principles, a smaller A_~f would be speed up the model checking process. An open repository called Buchi Store has been proposed recently, where numerous temporal formulae and their corresponding automata are collected. One can obtain the Buchi automaton of a desired formula by table look-up rather than applying translation algorithms. Since there will be hundreds or even thousands of formulae in the Buchi Store, an appropriate formulae classification is needed for the user to browse and search readily.

In this thesis, we study property transformation and classification methods, where properties are represented as formulae or automata. With the understanding of different classes of temporal properties, one can specify a program more completely and avoid underspecification. We implement the classification algorithm proposed by Manna and Pnueli in GOAL, which is a tool for creating, manipulating, and testing temporal formulae and Omega-automata, and apply the classification methods on formulae in the Buchi Store. These will make it easier for the user to search in the classified formulae. Moreover, checking the equivalence between two formulae or finding an equivalent formula for a given formula becomes easier, as two formulae are equivalent only if they belong to the same class. As a result, the capability of research and education will be enhanced in GOAL and the functionality of the Buchi Store will also be enriched.

並列關鍵字

Buchi Automata ； Buchi Store ； Classification ； GOAL ； Omega-Automata ； Temporal Logic ； Transformation ； Verification

參考文獻

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

[4] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of Workshop on Logic of Programs, LNCS 131, pages 52–71, 1981.

[5] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.

[8] R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification, pages 3–18. Chapman & Hall, 1995.

[10] G. J. Holzmann. The model checker SPIN. Software Engineering, 23(5):279–295, 1997.