傳統上，派屈網路分類的方式是依照區域結構分成"簡單網"、"非對稱選擇網"， "擴充自由選擇網"，"自由選擇網"，"標記圖形網"，"狀態機"。最近我們將派屈網路依照全域結構的分類方式分成兩類：同步選擇網及非同步選擇網。 同步選擇網的結構不同於其它的分類方式，不但可以作派屈網的分類，而且可以因此決定網路的性質如：boundedness、liveness、reversibility等。 在一個同步選擇網中，任何一個沒有bridge的handle必定是一個TT-或PP-路徑；同步選擇網也可以分解成許多T-components或P-components；同步選擇網是非常值得研究的題目，如果一個派屈網不屬於同步選擇網，這個派屈網很可能有設計上的錯誤如unbounded或deadlock。 / Traditionally Petri nets (PN) are classified, based on local structures (input and output set of transitions or places), into simple nets, asymmetric choice nets, extended free choice nets, free choice nets, mark graphs and state machines. We categorize ordinary Petri nets into two lasses: SNC and non-SNC based on global structure. Unlike other class of Petri nets, the structure of SNC nets not only classify the nets, but also determine the properties of the nets such as boundedness, liveness, reversibility, …etc. In an SNC, any prime handle must be either a TT-or PP-path. SNC nets is declared to be largest (than Free Choice) set of nets that are covered by both T-components and P-components. SNC nets is interesting because if a designed PN is not an SNC, then most likely it suffers from design errors of deadlocks or unbounded. SNC nets is both structurally live and bounded. However, it may not be live or reversible. This thesis presents the conditions of liveness and rsibility. An algorithm is developed to detect SNC nets which based on a useful mechanism called S-Matrix to records the structure relationship between any two PSP's. Further, we will also provide algorithms to check the SNC nets to be live and irreversible.

The Synchronize Choice Petri net, a subclass of Petri nets that is constructed based on special structural objects, can improve analytical power to make solving the behavioral problems of Petri nets practically possible. The fact that proving liveness and verifying reachability of a Synchronize Choice Petri net are feasible may lead to several applications. This thesis contributes to one of the applications: building a dynamic key exchange mechanism embedded in Virtual Private Network products by applying Synchronize Choice Petri nets. 　　Based on modern symmetric-key algorithms, such as DES, the dynamic key exchange mechanism enables two communicating sides to use the changing keys to encrypt or decrypt messages correctly without requiring any key transmission during the communication session after the initiation. A proper use of the mechanism is to be integrated with Virtual Private Network products to make the information transmitting between two peers more confidential.

The thesis contributes to the theoretical study of Petri net theory. We conduct boundedness and liveness structural analysis of Synchronized Choice nets (SNC) based on fundamental structures in Petri nets and identified as first-order structures. By studying these structures, the study proposes two ways of preserving good properties: addition of second-order structures or other asymmetric structures. Liveness of these new SNC nets is studied based on the concept of siphons and traps. We prove that SNC nets thus formed are structurally bounded and live. The thesis extends this class of nets to those with pure TP and PT first-order structures and explores its structural and marking conditions. Based on this, we introduce a new class of Synchronized Choice nets called Expanded Synchronized Choice nets.