有限溝通能力派屈網路之可達性分析

Abstract

在各類的派屈網路上可達性分析是一個很重要的議題，它可以用來分析活性問題， 公平性問題，可控性問題以及模型檢驗問題。在派屈網路的各種不同分析技巧法方法 上，我們覺得加上正規方法是非常合適用來描述各種系統。模型檢驗是檢查系統是否滿 足行為的一種自動方法。使用模型檢驗的觀念，我們可以簡單描述許多問題並且解決這 些有趣的問題。 在這篇論文，我們先針對擴增標示圖來做探討。擴增標示圖可以被想成是標示圖的 一種延伸並使其允許資源共享的狀況。擴增標示圖可以有用的塑模及分析某一類的彈性 製造系統。就我們所知，在傳統的派屈網路的分析技巧中用來分析擴增標示圖是用虹吸 式(siphon)。在這篇論文裡面，我們利用整數線性規劃的方法來分析某一類的擴增標示 圖就是所謂的可分解的擴增標示圖。我們展示了在一個可分解的擴增標示圖的路徑中其 可達性的問題可以被看成是解整數線性規劃的一個問題。我們更進一步的把我們的方法 擴充使其可以應用到某一類的分支時間時序邏輯與線性時間時序邏輯的模型驗證上。此 外，我們展示了我們的方法可以應用到彈性製造系統上的幾個範例。 其次，我們針對各種有限溝通能力派屈網路來進行可達性之分析。對無交談派屈網 路之可達性問題複雜度的問題已知是NP的問題。在沒有同步機制之下，這樣的無交談派 屈網路能力是被受限制的。因此，很重要的問題是是否可以增加無交談派屈網路的描述 能力之下而不犧牲其分析能力。在這篇論文中，我們從可判定性及複雜度的觀點為出發 點，來研究分析幾類無交談派屈網路變體中的可達性問題。這幾類無交談談派屈網路變 體其中包括了”靜態優先”、”動態優先”、”狀態” 、”禁止器弧”以及”時間限制” 。對許多擴充式無交談派屈網路而言，可達性問題變成比較困難去分析。事實上，對狀態 擴充式無交談派屈網路中加入優先權或禁止器弧而言，可達性的問題變成是不可判定性。 對於基本無交談派屈網路的模型，如果動態優先關係被利用到變遷實施上，其可達性的問 題還是不可判定性。

Reachability analysis is key to the solutions of a variety of Petri net problems including liveness, fairness, controllability, model checking and more. Among various analytical techniques of Petri nets, we feel that the approach based on formal methods is most suitable for flexible manufacturing systems. Model checking is an automatic technique for verifying that a behavior holds for a model of a system. Using the concept of model checking, it becomes feasible to describe and solve many interesting problems in practice. In the thesis, we first investigate augmented marked graphs. Augmented marked graphs (AMGs) can be thought of as extensions of marked graphs that allow resource sharing. It has been shown that AMGs are useful for modeling and analyzing certain types of flexible manufacturing systems. To our knowledge, the techniques developed for analyzing AMGs are mostly based upon checking certain Petri net structures such as siphons. This thesis exploits the integer linear programming approach for the analysis of a subclass of AMGs called decomposable AMGs. We show that reachability between two configurations of a decomposable AMG can be equated with solving an instance of integer linear programming. We further extend our technique to model checking a type of branching time temporal logics and a type of linear time temporal logics. Examples arisen in flexible manufacturing systems are used to demonstrate the application of our technique. Next, we study that the reachability issue of various Petri nets with limited communication capabilities. It is known that the reachability problem for communication-free Petri nets is NP-complete. Lacking the synchronization mechanism, the expressive power of communication-free Petri nets is somewhat limited. It is therefore important and interesting to see whether the power of communication-free Petri nets can be enhanced without sacrificing their analytical capabilities. As a first step towards this line of research, our main concern is to investigate, from the decidability/complexity viewpoint, the reachability problem for a number of variants of communication-free Petri nets, including communication-free Petri nets augmented with ‘static priorities,’‘dynamic priorities,’ ‘states’ ‘inhibitor arcs,’ and ‘timing constraints’. For most of the augmented communication-free Petri nets, the reachability problem becomes undecidable for stateextended communication-free Petri nets augmented with priority or inhibitor arcs. For the basic model of communication-free Petri nets, the reachability problem is also undecidable if a dynamic priority relation is imposed on transition firing.