Analysis of Reachability and Self-Stabilization for Some Infinite-State Systems

隨著系統具有分散式與平行處理的特性，當代系統設計與分析工作已變得越來越複雜。基本上，採用理論分析或實驗方式的解決方案是各有優缺點。理論分析的優點在於它的快速、精確、有效與省成本，其中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 . . . . . . . . . . . . . . . . . . . . . . 9