顏嗣鈞臺灣大學:電機工程學研究所陳建良Chen, Chien-LiangChien-LiangChen2010-07-012018-07-062010-07-012018-07-062009U0001-2101200915550900http://ntur.lib.ntu.edu.tw//handle/246246/187999在各類的派屈網路上可達性分析是一個很重要的議題，它可以用來分析活性問題，平性問題，可控性問題以及模型檢驗問題。在派屈網路的各種不同分析技巧法方法，我們覺得加上正規方法是非常合適用來描述各種系統。模型檢驗是檢查系統是否滿行為的一種自動方法。使用模型檢驗的觀念，我們可以簡單描述許多問題並且解決這有趣的問題。這篇論文，我們先針對擴增標示圖來做探討。擴增標示圖可以被想成是標示圖的種延伸並使其允許資源共享的狀況。擴增標示圖可以有用的塑模及分析某一類的彈性造系統。就我們所知，在傳統的派屈網路的分析技巧中用來分析擴增標示圖是用虹吸(siphon)。在這篇論文裡面，我們利用整數線性規劃的方法來分析某一類的擴增標示就是所謂的可分解的擴增標示圖。我們展示了在一個可分解的擴增標示圖的路徑中其達性的問題可以被看成是解整數線性規劃的一個問題。我們更進一步的把我們的方法充使其可以應用到某一類的分支時間時序邏輯與線性時間時序邏輯的模型驗證上。此，我們展示了我們的方法可以應用到彈性製造系統上的幾個範例。次，我們針對各種有限溝通能力派屈網路來進行可達性之分析。對無交談派屈網之可達性問題複雜度的問題已知是NP的問題。在沒有同步機制之下，這樣的無交談派網路能力是被受限制的。因此，很重要的問題是是否可以增加無交談派屈網路的描述力之下而不犧牲其分析能力。在這篇論文中，我們從可判定性及複雜度的觀點為出發，來研究分析幾類無交談派屈網路變體中的可達性問題。這幾類無交談談派屈網路變其中包括了”靜態優先”、”動態優先”、”狀態” 、”禁止器弧”以及”時間限制”對許多擴充式無交談派屈網路而言，可達性問題變成比較困難去分析。事實上，對狀態充式無交談派屈網路中加入優先權或禁止器弧而言，可達性的問題變成是不可判定性。於基本無交談派屈網路的模型，如果動態優先關係被利用到變遷實施上，其可達性的問還是不可判定性。Reachability analysis is key to the solutions of a variety of Petri net problems includingiveness, fairness, controllability, model checking and more. Among various analyticalechniques of Petri nets, we feel that the approach based on formal methods is most suitableor flexible manufacturing systems. Model checking is an automatic technique forerifying that a behavior holds for a model of a system. Using the concept of modelhecking, it becomes feasible to describe and solve many interesting problems in practice.n the thesis, we first investigate augmented marked graphs. Augmented markedraphs (AMGs) can be thought of as extensions of marked graphs that allow resourceharing. It has been shown that AMGs are useful for modeling and analyzing certainypes of flexible manufacturing systems. To our knowledge, the techniques developedor analyzing AMGs are mostly based upon checking certain Petri net structures such asiphons. This thesis exploits the integer linear programming approach for the analysisf a subclass of AMGs called decomposable AMGs. We show that reachability betweenwo configurations of a decomposable AMG can be equated with solving an instance ofnteger linear programming. We further extend our technique to model checking a typef branching time temporal logics and a type of linear time temporal logics. Examplesrisen in flexible manufacturing systems are used to demonstrate the application of ourechnique.ext, we study that the reachability issue of various Petri nets with limited communicationapabilities. It is known that the reachability problem for communication-freeetri nets is NP-complete. Lacking the synchronization mechanism, the expressive powerf communication-free Petri nets is somewhat limited. It is therefore important and interestingo see whether the power of communication-free Petri nets can be enhancedithout sacrificing their analytical capabilities. As a first step towards this line of research,ur main concern is to investigate, from the decidability/complexity viewpoint,he reachability problem for a number of variants of communication-free Petri nets, includingommunication-free Petri nets augmented with ‘static priorities,’‘dynamic priorities,’states’ ‘inhibitor arcs,’ and ‘timing constraints’. For most of the augmentedommunication-free Petri nets, the reachability problem becomes undecidable for stateextendedommunication-free Petri nets augmented with priority or inhibitor arcs. For theasic model of communication-free Petri nets, the reachability problem is also undecidablef a dynamic priority relation is imposed on transition firing.誌謝 i文摘要 ii文摘要 iv Introduction 1.1 Augmented Marked Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . . . . . 5.3 Organization of the Dissertation . . . . . . . . . . . . . . . . . . . . . . 7 Preliminaries 8.1 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.2 Petri Net Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12.2.1 Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12.2.2 Liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12.2.3 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14.3 Analytical Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . 15.3.1 State Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . 15.3.2 Net Unfoldings . . . . . . . . . . . . . . . . . . . . . . . . . . . 19.4 Augmented Marked Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 24 Reachability Analysis of AMGs 29.1 Reachability Analysis of AMGs by Linear Inequalities . . . . . . . . . . 29.2 Reachability Analysis of AMGs by Net Unfoldings . . . . . . . . . . . . 39 Model Checking 46.1 Unified System of Branching Time for Petri Nets . . . . . . . . . . . . . 47.2 Linear Time Temporal Logic for Petri Nets . . . . . . . . . . . . . . . . 50.3 Model Checking Using Net Unfoldings . . . . . . . . . . . . . . . . . . 52 Examples in Automated Manufacturing Systems 56 Variants of Communication-Free Petri Nets 74.1 State-Extended Communication-Free Petri Nets . . . . . . . . . . . . . . 74.2 Priority Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . 75.3 Communication-Free Petri Nets with Inhibitor Arcs . . . . . . . . . . . . 76.4 Clocked Communication-Free Petri Nets . . . . . . . . . . . . . . . . . . 77.5 Complexity and Decidability Analysis of the Reachability Problem . . . . 79.5.1 Priority Communication-Free Petri Nets . . . . . . . . . . . . . . 79.5.2 Communication-Free Petri Nets with Inhibitor Arcs . . . . . . . . 85.5.3 Communication-Free Clocked Petri Nets . . . . . . . . . . . . . 88 Conclusion 91eferences 931030982 bytesapplication/pdfen-US可達性問題擴增標示圖無交談派屈網路Reachability ProblemAugmented Marked GraphsCommunication-Free Petri Netsthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/187999/1/ntu-98-D89921027-1.pdf