Second Order Structures for Synchronized Choice Ordinary Petri Nets

摘要

Unlike traditional classification by output conditions of places, Synchronized Choice nets (SNC) were defined as a new class of nets characterized by bridges and handles. If a circuit Ω has a TP- (PT-) handle, H, then H is bridged to Ω through a PT- (TP-) bridge, B. It is rather difficult to verify this for arbitrary handles. It is, however, simpler to verify them for a class of nets where the above B is the only one that is bridged to Ω for each TP- (PT-) handle. We prove that this class of nets is equivalent to SNC. Such simple dual structures are used to discover the simple conditions of liveness and two kinds of minimal deadlocks for SNC. Based on which, we provide a formal proof of the liveness conditions based on the concept of deadlocks and traps. An integrated algorithm is presented for verification of SNC and liveness.