請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/41210完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤(Yih-Kuen Tsay) | |
| dc.contributor.author | Chi-Jian Luo | en |
| dc.contributor.author | 羅啟建 | zh_TW |
| dc.date.accessioned | 2021-06-14T17:24:05Z | - |
| dc.date.available | 2009-12-31 | |
| dc.date.copyright | 2008-07-30 | |
| dc.date.issued | 2008 | |
| dc.date.submitted | 2008-07-24 | |
| dc.identifier.citation | [1] Christoph Schulte Althoff, Wolfgang Thomas, and Nico Wallmeier. Observations on
determinization of Büchi automata. Theor. Comput. Sci., 363(2):224–233, 2006. [2] J.R. Büchi. 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] Y. Choueka. Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Science, pages 8:117–141, 1974. [4] Christof L‥oding. Methods for the transformation of ω-automata: Complexity and connection to second order logic. [5] Edmund M. Clarke and I. A. Draghicescu. Expressibility results for linear-time and branching-time logics. In REX Workshop, pages 428–437, 1988. [6] E.M. Clarke, I.A. Draghicescu, and R.P. Kurshan. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of Workshop on Logics of Programs, LNCS 131, pages 52–71, 1981. [7] E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999. [8] E. Muller David and E. Schupp Paul. Alternating automata on infinite trees. Theor. Comput. Sci., 54(2-3):267–276, 1987. [9] L. Doyen and J. F. Raskin. Improved algorithms for the automata-based approach to model-checking. In TACAS, pages 451–465, 2007. [10] E. Friedgut, O. Kupferman, and M.Y. Vardi. Büchi complementation made tighter. In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2004), LNCS 3299, pages 64–78. Springer, 2004. [11] D.M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In POPL ’80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 163–173, New York, NY, USA, 1980. ACM Press. [12] 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. [13] Erich Gr‥adel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. [14] S. Gurumurthy, O. Kupferman, F. Somenzi, and M. Vardi. On complementing nondeterministic Büchi automata. In CHARME, 2003. [15] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969. [16] Gerard J. Holzmann. The model checker SPIN. Software Engineering, 23(5):279–295, 1997. [17] G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison- Wesley, 2003. [18] Detlef K‥ahler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In ICALP (1), pages 724–735, 2008. [19] Nils Klarlund. Progress measures and finite arguments for infinite computations. PhD thesis, Ithaca, NY, USA, 1990. [20] Nils Klarlund. Progress measures for complementation of omega-automata with applications to temporal logic. In FOCS, pages 358–367, 1991. [21] Nils Klarlund. Liminf progress measures. In Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, pages 477– 491, London, UK, 1992. Springer-Verlag. [22] Nils Klarlund and Dexter Kozen. Rabin measures and their applications to fairness and automata theory. Technical report, Ithaca, NY, USA, 1991. [23] Joachim Klein and Christel Baier. Experiments with deterministic mega-automata for formulas of linear temporal logic. Theor. Comput. Sci., 363(2):182–195, 2006. [24] O. Kupferman and M. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, 2(3):408–429, 2001. [25] R.P. Kurshan. Complementing deterministic buchi automata in polynomial time. In Journal of Compututer and System Science, pages 35:59–71, 1987. [26] Lawrence H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3(4):376–384, 1969. [27] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safty. Springer, 1995. [28] M. Michel. Complementation is more difficult with automata on infinite words. In CNET, Paris, 1988. [29] S. Miyano and T. Hayashi. Alternating finite automata on ω-words. TCS, 32:321– 330, 1984. [30] David E. Muller. Infinite sequences and finite machines. In FOCS, pages 3–16, 1963. [31] David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata:new results and new proofs of the theorems of rabin, mcnaughton and safra. TCS, 141(1-2):69–107, 1995. [32] Nir Piterman. From nondeterministic Büchi and streett automata to deterministic parity automata. In LICS ’06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pages 255–264. IEEE Computer Society, 2006. [33] A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981. [34] M. O. Rabin and D. Scott. Finite automata and their decision problems. 3:115–125, 1959. [35] S. Rodger and T. Finley. JFLAP. http://www.jflap.org/. [36] S. Safra. On the complexity of ω-automta. In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1988), pages 319–327, 1988. [37] S. Safra and M. Y. Vardi. On ω-automata and temporal logic. In In Proc. 21th ACM Symp. on the Theory of Computing, 1989. [38] A.P. Sistla, M. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217– 237, 1987. [39] Wolfgang Thomas. Complementation of Büchi automata revisited. [40] Y.-K Tsay, Y.-F Chen, M.-H Tsai, K.-N Wu, and W.-C Chan. Goal: A graphical tool for manipulating buchi automata and temporal formulae. In TACAS ’2007: Tools and Algorithms for Construction and Analysis of Systems, 2007. [41] Y.-K. Tsay, Y.-F. Chen, and K.-N. Wu. Tool support for learning Büchi automata and linear temporal logic. Presented at the Formal Methods in the Teaching Lab Workshop, Hamilton, Canada, August 2006. [42] Moshe Y. Vardi. The Büchi complementation saga. In STACS, pages 12–22, 2007. [43] M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 332–344, 1986. [44] M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994. [45] Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1/2):72–99, 1983. [46] Qiqi Yan. Lower bounds for complementation of ω-automata via the full automata technique. In ICALP (2), pages 589–600, 2006. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/41210 | - |
| dc.description.abstract | 為Büchi自動機取補集在模型驗證中是一塊重要的領域。M. Michel在1988年就以提出此操作的理論最佳的上界為2O(n log n)，更精確的說是介於Ω((0.36n)n)。後人又得出更精確的理論界線介於Ω((0.76n)n)和O((0.97n)n)之間。從此便不斷有學者提出各種最佳化的補集演算法。這些演算法使用不同的技巧、自動機，並且產生出不一樣大小的補集自動機。因此到底哪一種演算法較好、較實用便成了許多學者探討的方向。但是盜墓錢為止都沒有一篇論文能夠較全面的比較每種演算法的實際運作，或者實際將各種演算法實做，並提供各種演算法的比較數據。
因此論文的第一個目的就是比較每種演算法的運作，為詳細的比較各個演算法，我們同時實做大部分的補集演算法，並用這些實做成果來跑比較實驗。在這些實驗中我們發現，一些演算法雖然沒有比較好的理論上界，但是在真實情況下通常比較有效率，像是Safra’s construction。同時在實做的過程中，我們也發現一些演算的的錯誤，並將其修正。我們發現各種補集演算法的交互檢查，給我們許多幫助和線索，這種檢查有助於提高實做的正確性以及檢查演算法自身的正確性。此外這篇論文的第二個目的則是讓人容易理解各種演算法的運作以及彼此之間的關聯性。因此我們將會詳細的介紹各種演算法，同時使用圖解的方式讓人們更容易理解演算法的運作。並使用演算法的關聯性，讓人們更容易融會貫通各種演算法。在實做方面，我們選擇GOAL作我們開發以及實驗的平台，GOAL是一套操作Omega自動機和時態邏輯的圖形工具，我們擴充六個補集演算法進這個工具。相信會改善這個工具的教育以及研究用途。 | zh_TW |
| dc.description.abstract | Büchi Complementation is a fundamental problem in the automata-theoretic approach
to model checking. The theoretically optimal upper bound is 2O(n log n) which is provided by M. Michel in 1988. The precise bound of Büchi complementation is ((0.36n)n). Then the tighter bounds are ((0.76n)n) which is provided by Qiqi Yan and O((0.97n)n) which is provided by O. Kupferman et al. The first optimal complementation algorithm was proposed by Safra in 1989. Since then a large number of optimal algorithms have been proposed. These algorithms construct Büchi automata using different intermediate automata and the constructed Büchi automata have different state spaces. Thus, there are some people proposed a few theoretical comparisons of Büchi complementation. These comparisons include explains of algorithms, but do not include the implementation of several algorithms and the experimental results. The first purpose of this thesis is to provide a more complete comparison of Büchi complementations. For comparative experiment, we implement these algorithms to compare these complementations. In these experiments, some algorithms have worse time complexity, but the efficiency of Büchi complementation is better such as Safra’s construction. A algorithm which is lower theoretical complexity does not guarantee that it is more efficient algorithm. We also find some bugs in these complementation algorithms when we implement them. It shows that the cross-checking between complementation methods is helpful to improve the accuracy of the implementations and check the correctness of the methods. The second purpose is to understand these algorithms how and why to do these Büchi complementations and explain these algorithms in detail. To describe them more clear, we use some examples and illustrations which show these algorithms in detail. In these examples, some relationships between these algorithms are also showed. These relationships help us to understand the Büchi complementation algorithms. The platform of the implementations is GOAL. For this research, we extend GOAL, a graphical tool for manipulating omega-automata and temporal formulae, with six complementation algorithms. The capability of research and education are also enhanced in GOAL. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-14T17:24:05Z (GMT). No. of bitstreams: 1 ntu-97-R95725029-1.pdf: 782762 bytes, checksum: 0d5b4a4bbd5ca932b56f1a58397c88f8 (MD5) Previous issue date: 2008 | en |
| dc.description.tableofcontents | 1 Introduction 1
1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Motivation and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Related Work and Preliminaries 4 2.1 Complementation Algorithms . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Kurshan’s Construction . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 Safra’s Construction . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.3 Via Weak Alternating Büchi Automata . . . . . . . . . . . . . . . 5 2.1.4 Via Weak Alternating Parity Automata . . . . . . . . . . . . . . . 6 2.1.5 Safra-Piterman Construction . . . . . . . . . . . . . . . . . . . . . 6 2.1.6 Progress Measure . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.7 Muller-Schupp Construction . . . . . . . . . . . . . . . . . . . . . 7 2.1.8 K‥ahler-Wilke Construction . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.1 JFLAP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.2 SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.3 GOAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Automata Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.2 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.3 Graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.4 Automata on Finite Words . . . . . . . . . . . . . . . . . . . . . . 13 2.3.5 Automata on Infinite Words . . . . . . . . . . . . . . . . . . . . . 14 2.3.6 Transition System . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.7 Acceptance Condition . . . . . . . . . . . . . . . . . . . . . . . . 17 2.4 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.4.1 Propositional Linear Temporal Logic (PTL) . . . . . . . . . . . . 25 2.5 Complementation of Büchi Automata . . . . . . . . . . . . . . . . . . . . 27 2.5.1 Unsound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5.2 Incomplete . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.5.3 Deterministic Büchi Automata . . . . . . . . . . . . . . . . . . . . 30 3 Methods of Determinization 32 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.2 Safra’s Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.2.1 Safra Tree . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.3 Safra-Piterman Construction . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.3.1 Compact Safra Tree . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.4 Muller-Schupp Construction . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.4.1 Muller-Schupp Tree . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.5 The Comparison of Safra, Safra-Piterman, and Muller-Schupp Construction 48 4 Methods of Progress Measure 53 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.2 Weak Alternating Büchi Automata . . . . . . . . . . . . . . . . . . . . . 53 4.2.1 Weak Alternating Büchi Automata . . . . . . . . . . . . . . . . . 53 4.2.2 Büchi Complementation via WABA . . . . . . . . . . . . . . . . . 56 4.3 Weak Alternating Parity Automata . . . . . . . . . . . . . . . . . . . . . 59 4.3.1 Weak Alternating Parity Automata . . . . . . . . . . . . . . . . . 59 4.3.2 Büchi complementation via WAPA . . . . . . . . . . . . . . . . . 62 4.4 Progress measure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4.4.1 Quasi Measure Automata . . . . . . . . . . . . . . . . . . . . . . 64 4.4.2 Büchi Complementation via Quasi Measure Automata . . . . . . 66 4.5 The Comparison of Progress Measure, WABA, and WAPA . . . . . . . . 66 5 Implementation and Experimental Results 70 5.1 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.1.2 Safra’s Construction . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.1.3 Complementation via WAPA and WABA . . . . . . . . . . . . . . 71 5.1.4 Safra-Piterman Construction . . . . . . . . . . . . . . . . . . . . . 71 5.1.5 Muller-Schupp Construction . . . . . . . . . . . . . . . . . . . . . 72 5.1.6 Kurshan’s Construction . . . . . . . . . . . . . . . . . . . . . . . 72 5.2 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 6 Conclusion 74 6.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 6.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 6.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 | |
| dc.language.iso | en | |
| dc.subject | 模型驗證 | zh_TW |
| dc.subject | Bü | zh_TW |
| dc.subject | chi自動機 | zh_TW |
| dc.subject | Omega自動機 | zh_TW |
| dc.subject | 驗證 | zh_TW |
| dc.subject | 決定化 | zh_TW |
| dc.subject | 補集 | zh_TW |
| dc.subject | Verfication | en |
| dc.subject | Model Checking | en |
| dc.subject | Complementation | en |
| dc.subject | Determinization | en |
| dc.subject | Bü | en |
| dc.subject | chi Automata | en |
| dc.subject | Omega-automata | en |
| dc.title | Büchi自動機補集演算法之比較研究 | zh_TW |
| dc.title | A Comparative Study of Algorithms for Büchi Complementation | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 96-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 陳恭(Kung Chen),王柏堯(Bow-Yaw Wang) | |
| dc.subject.keyword | 模型驗證,補集,決定化,Bü,chi自動機,Omega自動機,驗證, | zh_TW |
| dc.subject.keyword | Model Checking,Complementation,Determinization,Bü,chi Automata,Omega-automata,Verfication, | en |
| dc.relation.page | 82 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2008-07-26 | |
| dc.contributor.author-college | 管理學院 | zh_TW |
| dc.contributor.author-dept | 資訊管理學研究所 | zh_TW |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-97-1.pdf 未授權公開取用 | 764.42 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。