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

Abstract

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.