Liveness Conditions And Applications Of Some Subclasses Of S~*PR Nets

Resource Allocation System (RAS) is a typical kind of Discrete Event Systems (DES). Owing to the competition of limited shared resources, deadlocks often occurs in RAS, i.e. some processes may blocked because of the reason that these parts request for its advancement some resources currently held by some other parts in the set. Due to the graphical expression and the formalized mathematical descriptions, Petri nets which is a kind of mathematical modeling tools are wildly used to model and solve the deadlocks in RAS. S*PR nets, which are a subclass of Petri nets, have attracted much more attentions by its powerful modeling capabilities and have been applied to analyze the deadlock problem in RAS. The siphon-based liveness condition is an important research direction which can provide the theoretical foundation for the liveness test and liveness-enforcing supervisor design of S*PR nets. Currently, the research of liveness condition for S*PR nets is mainly aimed at an ordinary subclass named Gadara nets which are able to model RAS that has single resource requirement and has no relevance to any resources after a choice operation. However, it has been found that many common RAS should be modeled by other subclass of S*PR nets rather than Gadara nets. Therefore, this thesis defines three subclass of S*PR nets and introduced the liveness condition of them. The main contributions mainly divide into the following parts:(1) An ordinary subclass of S*PR nets named BS*PR net is proposed, which can model a class of resource allocation systems with buffers. A BS*PR net is live if all siphons of it are resource-controlled. On the basis of it, a mixed integer programming algorithm is proposed which can find non-resource-controlled siphons and can be utilized to test the liveness of BS*PR nets. Applications in multithreaded programs and classical manufacturing system show that BS*PR nets can effectively model and analyze a class of resource allocation systems with buffers.(2) An ordinary subclass of S*PR nets is defined as SEM-S*PR nets, which can model resource allocation systems that use resources symmetrically in the choice operations of the process. The choice places in a SEM-S*PR net can use resources symmetrically and there can be multiple copies of one kind of resources in the net. Thus, Gadara nets are a special case of SEM-S*PR nets naturally. Meanwhile, it is proved that a SEM-S*PR net is live if and only if all siphons of it are always marked during the execution of the net. Based on this conclusion, the mixed-integer programming tools can be applied to detect the liveness of SEM-S*PR nets. Furthermore, liveness condition of SEM-S*PR nets are extended to generalized S*PR nets named as OSC-S*PR nets, in which all the choice operation in the processes are symmetric as well. After proving that an OSC-S*PR net is live if all its siphons are Max’-Controlled, a mixed integer programming-based non-Max’-Controlled siphon test algorithm is proposed, which can test the liveness of OSC-S*PR nets. What’s more, the algorithm can also be utilized to test the liveness of S*PR nets by converting them into OSC-S*PR nets.The application results in real software systems, classical manufacturing systems and the philosopher problem show that the proposed subclasses of S*PR nets can not only be used to model and analysis the systems that modeled by Gadara nets, but can also to model the resources allocation systems which have symmetric choice operations or buffer operations. Meanwhile, on the basis of the liveness conditions, the mixed integer programming technique can also be applied to the liveness detection of S*PR nets which ensure a higher computational efficiency.