請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/38051完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 王凡(Farn Wang) | |
| dc.contributor.author | Chih-Hong Cheng | en |
| dc.contributor.author | 鄭志弘 | zh_TW |
| dc.date.accessioned | 2021-06-13T15:58:52Z | - |
| dc.date.available | 2008-06-05 | |
| dc.date.copyright | 2008-06-05 | |
| dc.date.issued | 2007 | |
| dc.date.submitted | 2008-05-19 | |
| dc.identifier.citation | [1] T. Ball, S.K. Rajamani. Automatically Validating Temporal Safety Properties of Interfaces. SPIN Workshop on Model Checking of Software, May 2001, LNCS 2057, Springer-
Verlag, pp. 103-122. [2] F. Buccafurri, T. Eiter, G. Gottlob, N. Leone. Enhancing Model Checking in Verification by AI Techniques, Artificial Intelligence, 112 (1), 1999, pp. 55-93. [3] R.E. Bryant Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers. VOL. 35, NO. 8, pp. 677-691, 1986. [4] H. Bunke. On a Relation between Graph Edit Distance and Maximum Common Subgraph. Pattern Recognition Letters. 19(1997) pp. 255-259. [5] E.M. Clarke, O. Grumberg, D.A. Peled. Model checking. The MIT Press, 2001. [6] D. Conte, P. Foggia, C. Sansone, M. Vento. Thirty Years of Graph Matching in Pattern Recognition, International Journel of Pattern Recognition and Artificial Intelligence, VOL. 18, NO. 5, pp. 265-298. [7] Y. Ding, Y. Zhang. A Logic Approach for LTL System Modification, Foundations of Intelligent Systems, LNCS 3488, Springer-Verlag. [8] Y. Ding, Y. Zhang. Algorithms for CTL System Modification. The 9’th Conference on Knowledge-Based Intelligent Information and Engineering Systems (KES), Aug. 2005, LNCS 3682, Springer-Verlag. [9] A. Dovier, C. Piazza. The Subgraph Bisimulation Problem, IEEE Transactions on Knowledge and Data Engineering, VOL. 15, NO. 4, pp. 1055-1056. [10] K. Fisler, M. Y. Vardi. Bisimulation Minimization in an Automata-Theoretic Verification Framework, FMCAD ’98, LNCS 1522, Springer-Verlag. [11] E. Gradel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games, LNCS 2500, Springer-Verlag. [12] A. Griesmayer, R. Bloem, and B. Cook . Repair of Boolean Programs with an Application to C. CAV’2006, LNCS 4144, Springer-Verlag. [13] http://javaddlib.sourceforge.net/jdd/ [14] http://www.jgraph.com [15] B. Jobstmann, A. Griesmayer, R. Bloem. Program Repair as a Game. CAV’2005, LNCS 3576, Springer-Verlag. [16] L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. [17] R. Milner. An Algebraic Defnition of Simulation between Programs, Proceedings of the 2nd International Joint Conference on Artificial Intelligence, 1971. [18] G. J. Myers, C. Sandler, T. Badgett, and T. M. Thomas. The Art of Software Testing. Wiley, 2004. [19] R. Paige, R.E. Tarjan, Three Partition Refinements Algorithms, SIAM J. Computing, VOL. 16, NO. 6, pp. 973-989, 1987. [20] A. Pnueli, R. Rosner. On the Synthesis of a Reactive Module. POPL’89, ACM Press, pp. 179-190. [21] A. Pnueli, A Temporal Logic of Concurrent Programs. Theoretical Computer Science 13: 45-60. [22] W. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, VOL. 4, 1970, pp. 177-192. [23] http://www.ifi.unizh.ch/ddis/research/semweb/simpack/ [24] 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. TACAS’2007, to appear in the LNCS series, Springer-Verlag. [25] G. Valiente. Algorithms on Trees and Graphs, Springer-Verlag, 2002. [26] M.Y. Vardi, P. Wolper. An automata-theoretic approach to automatic program verification. Proceedings of 1st Symposium on Logic in CS, pp.332-344, Cambridge, June 1986. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/38051 | - |
| dc.description.abstract | We combine the graph theory and the automaton theory for a general research framework of automatic system repair. This new framework not only allows us to analyze all system repairs expressible with B‥uchi automata but also can help us telling‘economic’repairs from‘expensive’repairs. Three criteria for model repair are proposed: repair for language containment, repair for language equivalence, and repair for bisimulation equivalence. We borrow the concept of graph-edit distance in the graph theory to define the repair cost for a system automaton. We establish the complexities of the problems of finding correct model repairs with minimum cost with the three criteria. We then present an algorithm that uses a breadth first approach to explore the repair space to solve the problem for a repair criterion. We also present a heuristic algorithm for bisimulation. Finally, we report our experiment that checks the performance of our algorithms. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-13T15:58:52Z (GMT). No. of bitstreams: 1 ntu-96-R94921104-1.pdf: 340675 bytes, checksum: 1eea4e61574c66c80f70c5e00e402df0 (MD5) Previous issue date: 2007 | en |
| dc.description.tableofcontents | Contents i
List of Figures iii List of Tables iv Acknowledgements v 1 Introduction 1 2 B‥uchi Automata and Their Repairs 4 3 An Upper-Bound on Minimum Model Repair 8 4 Criteria for Model Repair 16 4.1 Repair for language containment 16 4.2 Repair for language equivalence 19 4.3 Repair for bisimulation equivalence 20 5 Algorithmic Issues 24 5.1 An exploration algorithmfor minimum-cost repair 24 5.2 An algorithmfor calculating the upper-bound of repair 25 5.3 AnMCS-based algorithm for repair for bisimulation 28 5.3.1 Step 1: minimizing Aψ − GMCS 29 5.3.2 Step 2: maximizing the reusability in the difference of AM 30 6 Implementation and Experiments 34 7 Related Works 36 8 Conclusions 38 A A logic based algorithm to find repair for maximizing the reusability in the difference of AM 39 B An overview of ModelRepair v.0.1 41 B.1 Input format 41 B.2 Basic functionalities 42 B.3 ModelRepair Simple Instructions 43 Bibliography 44 | |
| dc.language.iso | en | |
| dc.subject | 自動機 | zh_TW |
| dc.subject | 修復技術 | zh_TW |
| dc.subject | repair | en |
| dc.subject | automata | en |
| dc.title | 以自動機理論發展之最小模型修復技術 | zh_TW |
| dc.title | Minimum Model Repair with an Automata-Theoretical Approach | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 96-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 黃鐘揚(Chung-Yang Huang),江介宏(Jie-Hong Roland Jiang),呂學一(Hsueh-I Lu),蔡益坤(Yih-Kuen Tsay) | |
| dc.subject.keyword | 自動機,修復技術, | zh_TW |
| dc.subject.keyword | automata,repair, | en |
| dc.relation.page | 45 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2008-05-21 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-96-1.pdf 未授權公開取用 | 332.69 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。