時序邏輯至自動機轉換演算法之深入比較研究

A Comprehensive Comparison of Temporal Formula to Automaton Translation Algorithms

張晉碩(Jinn-Shu Chang)

指導教授 ： 蔡益坤

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

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

摘要

無資料

關鍵字

Büchi自動機 ； GOAL ； 模型驗證 ； Omega自動機 ； 時序邏輯 ； 程式驗證

並列摘要

Translation of a temporal formula into an automaton is a central issue in the automatabased approach to model checking. In the approach, model checking of a system M against a temporal specification f proceeds in three steps: (1) generate an automaton A¬f for the negation of f, (2) construct a product automaton A that is the intersection of
M and A¬f , and (3) check the emptiness of the product automaton A. The time needed to complete the model checking task is proportional to the size of A, which is the product
of the sizes of M and A¬f . For a given system, the size of A¬f determines the size of A. Therefore, the smaller A¬f is, the faster the model checking task may be carried out.
In this thesis, we investigate an extensive collection of translation algorithms, including all of the well-known ones. We compare the state and the transition sizes of
the automata generated from these algorithms. An algorithm that generates smaller automata should be more helpful when it is applied in model checking. The reason is that when one needs to certify that a system satisfies the desired property, the complete product automaton must be constructed. To perform the comparison, we implement not
only the translation algorithms but also possible improvements in the GOAL tool. From the experimental results, we observe that none of the algorithms can always generate the smallest automaton for each of the temporal formulae considered. We therefore propose a portfolio for choosing suitable algorithms for different kinds of temporal formulae. We also design and implement an open repository called B‥uchi Store where one can look up
the B‥uchi automaton for a given temporal formula.

並列關鍵字

Büchi Automata ； GOAL ； Model Checking ； Omega-Automata ； Temporal Logic ； Verification

參考文獻

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

Patterns. http://patterns.projects.cis.ksu.edu/.

[2] J.R. B‥uchi. On a decision method in restricted second-order arithmetic. In Proceedings

of the International Congress on Logic, Methodology and Philosophy of Science,

[3] W.-C. Chan. A comparative study of algorithms for linear temporal logic to B‥uchi