請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8794完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤(Yih-Kuen, Tsay) | |
| dc.contributor.author | Jinn-Shu Chang | en |
| dc.contributor.author | 張晉碩 | zh_TW |
| dc.date.accessioned | 2021-05-20T20:01:26Z | - |
| dc.date.available | 2009-12-31 | |
| dc.date.available | 2021-05-20T20:01:26Z | - |
| dc.date.copyright | 2009-12-29 | |
| dc.date.issued | 2009 | |
| dc.date.submitted | 2009-11-20 | |
| dc.identifier.citation | [1] H. Alavi, G. Avrunin, J. Corbert, L. Dillon, M. Dwyer, and C. Pasareanu. Spec
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, pages 1–11. Standford University Press, 1962. [3] W.-C. Chan. A comparative study of algorithms for linear temporal logic to B‥uchi automata translation, 2007. [4] Y. Choueka. Theories of automata on !-tapes: A simplified approach. Journal of Computer and System Science, pages 8:117–141, 1974. [5] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. [6] J.-M. Couvreur. On-the-fly verification of linear temporal logic. In World Congress on Formal Methods, LNCS 1708, pages 253–271. Springer, 1999. [7] M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for linear temporal logic. In Proceedings of the 11th International Conference on Computer- Aided Verification (CAV 1999), LNCS 1633, pages 249–260, 1999. [8] P. Gastin and D. Oddoux. Fast LTL to B‥uchi automata translations. In Proceedings of the 13th International Conference on Computer-Aided Verification (CAV 2001), LNCS 2102, pages 53–65. Springer, 2001. [9] 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] D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of LTL formulae to b‥uchi automata. In Formal Techniques for Networked and Distributed Sytems, LNCS 2529, pages 308–326. Springer-Verlag, 2002. [11] G. J. Holzmann. The model checker SPIN. Software Engineering, 23(5):279–295, 1997. [12] G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison- Wesley, 2003. [13] Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In Proceedings of the 5th International Conference on Computer-Aided Verification (CAV 1993), LNCS 697, pages 97–109. Springer, 1993. [14] Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, 163(1):203–243, 2000. [15] O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: From lineartime to branching-time. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS 1998), pages 81–92. Springer, 1998. [16] O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000. [17] Z. Manna and A. Pnueli. A hierarchy of temporal properties. Technical Report STAN-CS-87-1186, Stanford University, Department of Computer Science, 1987. [18] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995. [19] S. Miyano and T. Hayashi. Alternating finite automata on !-words. Theoretical Computer Science, 32:321–330, 1984. [20] D. E. Muller. Infinite sequences and finite machines. In Proceedings of the 4th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1963), pages 3–16, 1963. [21] A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981. [22] R. Sebastiani and S. Tonetta. “more deterministic” vs. “smaller” B‥uchi automata for efficient LTL model checking. In Correct Hardware Design and Verification Methods, pages 126–140, 2003. [23] F. Somenzi and R. Bloem. Efficient B‥uchi automata from LTL formulae. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV 2000), LNCS 1855, pages 248–263. Springer, 2000. [24] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega automata and temporal logic. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, pages 346–350. Springer, 2008. [25] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, W.-C. Chan C.-J. Luo, and J.-S. Chang. Tool support for learning b‥uchi automata and linear temporal logic. Formal Aspects of Computing, 21(3):259–275, 2009. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8794 | - |
| dc.description.abstract | 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. | en |
| dc.description.provenance | Made available in DSpace on 2021-05-20T20:01:26Z (GMT). No. of bitstreams: 1 ntu-98-R96725010-1.pdf: 726249 bytes, checksum: 3795acc5b49fdbcf0e8199869a90b4f4 (MD5) Previous issue date: 2009 | en |
| dc.description.tableofcontents | Contents
1 Introduction . . . . . . . . . . . . . . . . . . . . . .1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Motivation and Objectives . . .. . . . . . . . . . . . 2 1.3 Thesis Outline . . . . . . . . . . . . . . . . . . . . 3 2 Preliminaries . . . . . . . . . . . . . . . . . . . . . 5 2.1 Automata on Infinite Words . . . . . . . . . . . . . . 5 2.2 Variants of omega-automata . . . . . . . . . . . . . . 7 2.2.1 Büchi Automata . . . . . . . . . . . . . . . . . . . 7 2.2.2 Generalized Büchi Automata . . . . . .. . . . . . . 9 2.2.3 Transition-Based Generalized Büchi Automata . . . 10 2.2.4 Co-B‥uchi Very Weak Alternating Automata . . . . .. 10 2.3 Propositional Linear Temporal Logic (PTL) . . . . . . 10 3 Related Work . . . . .. . . . . . . . . . . . . . . . . 14 3.1 Translation Algorithms . . . . . . . . . . . . . . . 14 3.1.1 Couvreur’s Algorithm . . . . . . . . . . . . . . 14 3.1.2 LTL2BA . . . . . .. . . . . . . . . . . . . . . . . 15 3.1.3 LTL2BUCHI . . . . . . . . . . . . . . . . . . . . . 15 3.1.4 GPVW+ . . . . . . . . . . . . . . . . . . . . . . . 16 3.1.5 LTL2AUT+ . . . . .. . . . . . . . . . . . . . . . . 16 3.1.6 MoDeLLa . . . . . . . . . . . . . . . . . . . . . . 16 3.2 Tools . . . . . . . . . . . . . . . . . . . . . . . . 17 3.2.1 SPIN . . . . . . . . . . . . . . . . . . . . . . . 17 3.2.2 GOAL . . . . . . . . . . . . . . . . . . . . . . . 18 4 Translation Algorithms . . . . . . . . . . . . . . . . 21 4.1 Couvreur’s Algorithm . . . . . . . . . . . . . . . . 21 4.2 LTL2BA . . . . . . . . . . . . . . . . . . . . . . . 24 4.2.1 LTL to VWAA . . . . . . . . . . . . . . . . . . . 24 4.2.2 VWAA to TGBA . . . . . . . . . . . . . . . . . . . 26 4.2.3 TGBA to BA . . . . . . . . . . . . . . . . . . . . 27 4.3 LTL2BUCHI . . . . . . . . . . . . . . . . . . . . . . 28 4.3.1 Data Structure . . . . . . . . . . . . . . . . . . 28 4.3.2 Algorithm . . . . . . . . . . . . . . . . . . . . . 29 4.4 MoDeLLa . . . . . . . . . . . . . . . . . . . . . . . 32 4.4.1 Determining the covers . . . . . . . . . . . . . . 35 4.4.2 Algorithm . . . . . . . . . . . . . . . . . . . . . 36 5 Experimental Results . . . . . . . . . . . . . . . . . 39 5.1 Settings of the Experiment . . . . . . . . . . . . . 39 5.2 Results . . . . . . . . . . . . . . . . . . . . . . . 39 6 Discussion and Implication . . . . . . . . . . . . . . .54 6.1 Portfolio . . . . . . . . . . . . . . . . . . . . . . 56 6.2 Büchi Store . . . . . . . . . . . . . . . . . . . . . 57 7 Conclusion . . . . . . . . . . . . . . . . . . . . . . .58 7.1 Contributions . . . . . . . . . . . . . . . . . . . . 58 7.2 Future Work . . . . . . . . . . . . . . . . . . . . . 60 Bibliography . . . . . . . . . . . . . . . . . . . . . . . .61 | |
| dc.language.iso | zh-TW | |
| dc.title | 時序邏輯至自動機轉換演算法之深入比較研究 | zh_TW |
| dc.title | A Comprehensive Comparison of Temporal
Formula to Automaton Translation Algorithms | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 98-1 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 顏嗣鈞(Hsu-Chun, Yen),王凡(Farn Wang) | |
| dc.subject.keyword | Bü,chi自動機,GOAL,模型驗證,Omega自動機,時序邏輯,程式驗證, | zh_TW |
| dc.subject.keyword | Bü,chi Automata,GOAL,Model Checking,Omega-Automata,Temporal Logic,Verification, | en |
| dc.relation.page | 63 | |
| dc.rights.note | 同意授權(全球公開) | |
| dc.date.accepted | 2009-11-20 | |
| dc.contributor.author-college | 管理學院 | zh_TW |
| dc.contributor.author-dept | 資訊管理學研究所 | zh_TW |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-98-1.pdf | 709.23 kB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。