跳到主要內容

臺灣博碩士論文加值系統

(18.97.14.87) 您好!臺灣時間:2025/02/17 12:49
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:于濂波
研究生(外文):Lien-Po Yu
論文名稱:無窮狀態系統的可到達性與自穩定性分析
論文名稱(外文):Analysis of Reachability and Self-Stabilization for Some Infinite-State Systems
指導教授:顏嗣鈞
學位類別:博士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2005
畢業學年度:94
語文別:英文
論文頁數:96
中文關鍵詞:複雜度可控制性分解式策略可決定性無窮狀態系統派翠網可到達性自穩定性評價方法驗證
外文關鍵詞:ComplexityControllabilityDecomposition strategyDecidabilityInfinite-state systemPetri netReachabilitySelf-stabilizationValuation methodVerification
相關次數:
  • 被引用被引用:0
  • 點閱點閱:503
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
隨著系統具有分散式與平行處理的特性,當代系統設計與分析工作已變得越來越複雜。基本上,採用理論分析或實驗方式的解決方案是各有優缺點。理論分析的優點在於它的快速、精確、有效與省成本,其中Petri網(Petri nets)應可視為從事分散式與平行處理系統塑模(Modeling)與分析最成功的正規(Formal)與圖形工具之一,目前Petri網已廣泛地被工業界、學術界及其他許多領域所應用。本研究的主要目的係針對分散式及/或平行處理系統的幾個重要問題,探索一致化的理論分析策略。相關研究工作與成果包括:

1.首先針對一類所謂的簡單迴路Petri網(Simple-circuit Petri net)的可到達性(Reachability)問題的複雜度(Complexity) 加以探討,並以一種分解式策略(Decomposition strategy)分析得到此類Petri網的可到達性問題屬NP-complete。由於簡單迴路Petri 網包含了例如Conflict-free、Normal [15, 36]、BPP-net [40]及Trap-circuit [16, 39]等Petri網,故這樣的策略就意義而言是屬於一種一致化的分析策略。 另外,有關一些時間性的邏輯(Temporal logics)的模型驗證(Model checking)問題也一併在此處探討。
2.自穩定性(Self-stabilization)可看成是一種容錯(Fault-tolerance)性質;它允許分散式系統容忍瞬時錯誤。本研究接著從可決定性(Decidability) 的觀點分析了一系列無窮狀態系統(Infinite-state systems)的自穩定性問題,並利用一種以週期行為基礎的分析策略得到:Lossy vector addition systems with states、One-counter machines及 Confict-free Petri nets等無窮狀態系統的自穩定性性質是可決定的(Decidable);另一方面對於Lossy counter machines及Lossy channel systems則是不可決定的(Undecidable)。
3.最後,針對隨機Confict-free Petri nets所建立的無窮狀態系統模型,探討了一些與可靠性分析(Dependability analysis)密切關聯的問題,並得到諸如Termination with probability 1、Self-stabilization with probability 以及Controllability with probability等問題也可以用一種以評價方法(Valuation method)為基礎的分析策略得到解決。
Petri nets, being regarded as one of the most successful formal and graphical tools for modeling and analyzing of distributed and/or concurrent systems, are extensively applied by industry, academia, and many other areas during the past years. The primary purpose of the research is to provide a better insight into the domain of analytic solutions to complex systems through the exploration of unified strategies for the analysis of several important problems for a variety of prevalent models for distributed and/or concurrent systems. The work done and contributions made by the research include:

1. The complexity of the reachability problem is studied for a new subclass of Petri nets called simple-circuit Petri nets. By taking advantage of the circuit structures, a new decomposition strategy is used to develop an integer linear programming formulation for characterizing the reachability sets of this class of Petri nets. Consequently, the reachability problem is shown to be NP-complete. As this class of Petri nets properly contains several well known subclasses such as conflict-free, normal, BPP-net, trap-circuit, the decomposition strategy thus has in a sense provided a new unifying proof showing NP-completeness of the reachability problem of different subclasses of PNs that had their own independent proofs. The model checking problem for some temporal logics is also investigated.

2. Self-stabilization can be regarded as a particular form of fault-tolerance in distributed systems that can tolerate transient faults. The problem of deciding whether a given system is self-stabilizing or not is investigated, from the decidability viewpoint, for a variety of infinite-state systems. A unified periodic behavior-based strategy is developed so that checking self-stabilization is shown to be decidable for lossy vector addition systems with states, one-counter machines, and conflict-free Petri nets, while undecidable for lossy counter machines and lossy channel systems.

3. A number of problems closely related to dependability analysis in the context of probabilistic infinite-state systems modeled by probabilistic conflict-free Petri nets are discussed. Using a valuation method, it is shown that the problems of termination with probability 1, self-stabilization with probability 1, as well as controllability with probability 1 can be solved in a unified framework.
Chapter 1: Introduction
1.1 Overview of the Problem . . . . . . . . . . . . . . . 1
1.2 Purpose and Importance of the Study. . . . . . . . . 2
1.3 Related Work . . . . . . . . . . . . . . . . . . . . 4
1.4 Organization of the Dissertation . . . . . . . . . . 10
Chapter 2: Preliminaries
2.1 Basic Terms . . . . . . . . . . . . . . . . . . . . 12
2.2 Petri Nets . . . . . . . . . . . . . . . . . . . . . 13
2.3 Other Infinite-state Systems . . . . . . . . . . . . 25
2.4 Problems under Investigation . . . . . . . . . . . . 29
Chapter 3: Decomposition Strategy for Reachability Analysis
3.1 Decomposition Strategy . . . . . . . . . . . . . . . 35
3.2 Characterizing sc-PN Computations using ILP. . . . . 40
3.3 Model Checking . . . . . . . . . . . . . . . . . . . 57
3.4 Summary. . . . . . . . . . . . . . . . . . . . . . . 58
Chapter 4: Decidability Analysis of Self-stabilization
4.1 Periodic Behavior-based Strategy . . . . . . . . . . 61
4.2 Decidability Analysis of Self-stabilization of Infinite-State Systems. . . . . . . . . . . . . . . . . . . . . . 65
4.3 Summary. . . . . . . . . . . . . . . . . . . . . . . 78
Chapter 5: Valuation-based Strategy for Dependability Analysis
5.1 Valuation-based Strategy . . . . . . . . . . . . . . 80
5.2 Dependability Analysis of pcf-PNs. . . . . . . . . . 84
5.3 Summary. . . . . . . . . . . . . . . . . . . . . . . 88
Chapter 6: Conclusions and Future Work
6.1 Summary of Contributions . . . . . . . . . . . . . . 89
6.2 Future Research. . . . . . . . . . . . . . . . . . . 91

Bibliography . . . . . . . . . . . . . . . . . . . . . . 93
[1] R. Alur and D. Dill, "A theory of timed automata", Theoret. Comput. Sci., 126, pp.183-235, 1994.
[2] P. Abdulla and B. Jonsson, "Undecidable verification problems for programs with unreliable channels", Inform. and Comput., 130, pp.71-90, 1996.
[3] A. Bouajjani and R. Mayr, "Model checking lossy vector addition systems", Proc. of STACS''99, LNCS 1563, pp.323-333, 1999.
[4] G. Cece, A. Finkel and S. Iyer, "Unreliable channels are easier to verify than perfect channels", Inform. and Comput., 124(1), pp.20-31, 1996.
[5] L. Cherkasova, R. Howell and L. Rosier, "Bounded self-stabilizing Petri nets", Acta Informatica, 32, pp.189-207, 1995.
[6] E. Clarke, O. Grumberg and D. Long, "Veri‾cation Tools for Finite-State Concurrent Systems", Lecture Notes in Computer Science, 803, Springer-Verlag, pp.124-175, 1994.
[7] L. Dickson, "Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors", Amer. J. Math., 35, pp.413-422, 1913.
[8] E. Dijkstra, "Self-stabilizing systems in spite of distributed control", C. ACM, 17, pp.643-644, 1974.
[9] S. Ginsburg, "The mathematical theory of context-free languages", McGraw-Hill, 1966.
[10] M. Gouda, R. Howell and L. Rosier, "The instability of self-stabilization", Acta Informatica, 27, pp.697-724, 1990.
[11] T. Herman, "A comprehensive bibliography on self-stabilization", http://www.cs.uiowa.edu/ftp/selfstab/bibliography), Chicago Journal of Theoretical Computer Science, 1998.
[12] L. Holloway and B. Krogh, "Controlled Petri nets: a tutorial survey", Discrete Event Systems, Lecture Notes in Control and Information Sciences, 199, G. Cohen and J.-P. Quadrat (eds.), pp.158-168, Springer-Verlag, 1994.
[13] J. Hopcroft and J. Pansiot, "On the reachability problem for 5-dimensional vector addition systems", Theoret. Comput. Sci., 8(2), pp.135-159, 1979.
[14] R. Howell and L. Rosier, "On questions of fairness and temporal logic for conflictfree Petri nets", in G. Rozenberg, editor, Advances in Petri Nets, LNCS 340, pp.200-226, Springer-Verlag, Berlin, 1988.
[15] R. Howell, L. Rosier and H. Yen, "Normal and sinkless Petri nets", Journal of Computer and System Sciences, 46, pp.1-26, 1993.
[16] A. Ichikawa and K. Hiraishi, "Analysis and control of discrete event systems represented by Petri nets", LNCIS 103, pp.115-134, 1987.
[17] R. Kosaraju, "Decidability of reachability in vector addition systems", Proc. the 14th Annual ACM Symposium on Theory of Computing, pp.267-280, 1982.
[18] R. Kumar and V. K. Garg, "Control of stochastic discrete event systems modeled by Probabilistic languages", IEEE Transaction on Automatic Control, 46(4), pp.593-606, 2001.
[19] P. Kungas, "Resource-conscious AI planning with conjunctions and disjunctions", Acta Cybernetica, 15(4), pp.601-620, 2002.
[20] L. Landweber and E. Robertson, "Properties of con°ict-free and persistent Petri nets", J. ACM 25(3), pp.352-364, 1978.
[21] R. Lipton, "The reachability problem requires exponential space", Technical Report 62, Yale University, Dept. of CS., Jan. 1976.
[22] M. Lawford and W. M. Wonham, "Supervisory control of probabilistic discrete event systems", Proc. 36th Midwest Symp. Circuits Systems, pp.327-331, 1993.
[23] M. A. Marsan, G. Balbo, G. Conte, S. Donatelli and G. Franceschinis, "Modeling with generalized stochastic petri nets", John Wiley & Sons, 1995.
[24] T. Matsumoto and Y. Mayano, "Reachability criterion for Petri nets with known‾ring vectors", IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. 81-A, No. 4, pp.628-634. 1998.
[25] E. Mayr, "An algorithm for the general Petri net reachability problem", SIAM J. Comput. 13, pp.441-460, 1984.
[26] R. Mayr, "Undecidable problems in unreliable computations", Theoret. Comput. Sci., 1-3(297), pp.337-354, 2003.
[27] T. Murata, "Petri nets: properties, analysis and applications", Proc. of the IEEE, 77(4), pp.541-580, 1989.
[28] H. Olsen, "Automatic veri‾cation of Petri nets in a CLP framework", Ph.D. Thesis, Dept. of Computer and Information Science, IDA, LinkÄoping Univ., 1997.
[29] J. Peterson, "Petri Net Theory and the Modeling of Systems", Prentice Hall, Englewood Cli®s, NJ, 1981.
[30] M. Presburger, ""Uber die vollstÄandigkeit eines gewissen systems der arithmetik...", Comptes rendues du premier Congres des Math. des Pays Slaves, Warsaw, pp.92-101, 395, 1929.
[31] P. Ramachandran and M. Kamath, "A sufficient condition for reachability in a general Petri net", Discrete Event Dynamic Systems, vol. 14, no. 3, pp.251-266, July 2004.
[32] W. Reisig, "Petri Nets: An Introduction", Springer-Verlag, New York, 1985.
[33] L. Rosier and H. Yen, "Logspace hierarchies, polynomial time and the complexity of fairness problems concerning w-machines", SIAM J. Computing, 16(5), pp.779-
807, 1987.
[34] D. Schmidt, "Denotational Semantics", Allyn and Bacon, 1986.
[35] R. Valk and M. Jantzen, "The Residue of Vector Sets with Applications to Decidability in Petri Nets", Acta Informatica, 21, pp.643-674, 1985.
[36] H. Yamasaki, "Normal Petri nets", Theor. Comput. Sci., 31, pp.307-315, 1984.
[37] H. Yen, B.Wang and M. Yang, "Deciding a class of path formulas for conflict-free Petri nets", Theory of Computing Systems, 30(5), pp.475-494, 1997.
[38] H. Yen, "A unified approach for deciding the existence of certain Petri net paths", Inform. and Comput., 96(1), pp.119-137, 1992.
[39] H. Yen, "On the regularity of Petri net languages", Inform. and Comput., 124(2), pp.168-181, 1996.
[40] H. Yen, "On reachability equivalence for BPP-nets", Theoretical Computer Science, 179, pp.301-317, 1997.
[41] H. Yen, "A valuation-based analysis of conflict-free Petri nets", Systems and Control Letters, 45(5), pp.387-395, 2002.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top