Reachability Analysis of Petri Nets with Limited Communication Capabilities

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.