當編輯派翠網時有效率維護發生圖之方法

Abstract

隨著資訊時代的進步，各類系統愈來愈複雜，分析這些系統正確性的方法好壞變得很重要。執行一個方法的需求時間也是這個方法好壞的一個關鍵點。派翠網是一種可以被用來分析許多系統的模型，而發生圖是派翠網的狀態圖。一個派翠網的發生圖可以被用來分析許多這個派翠網的特性。這篇論文提出了一個技術：當編輯派翠網時利用維護原本的發生圖來縮短建立新發生圖的時間。根據派翠網的語意，本文討論到的編輯動作包含：新增、刪除、合併各項派翠網元件。為了保持派翠網語意上的正確性，每個編輯的動作可能是一或一組點或線的自動編輯動作。相對的，當一些使用發生圖的分析方法需要取得發生圖時即可節省時間。

Petri Net can model many kinds of systems. An occurrence graph is the state diagram of a Petri net. It can show useful properties such as reachability, boundness, home, liveness, and fairness. This thesis presents a technique that reduces the occurrence graph building time by maintaining current, instead of constructing new O-graph of a Petri net when an edit action is done. The maintenance is based on three groups of edit actions: (1) addition of a(n) node, arc, or token, (2) deletion of a(n) node, arc, or token, (3) mergence of places or transitions where each of them represents a or a sequence of addition/deletion of place, transition, and/or arc. The maintenance algorithm, proof, and time complexity for each edit action are discussed respectively.