Research On Constraint Programming Based Petri Net's Reachability Problem

Petri net is a graphical and mathematical modeling tool applicable to many systems. It isa promising tool for the systems that are characterized as being concurrent, asynchronous,distributed, parallel, nondeterministic, and/or stochastic. The reachability problem is one ofthe basic problems in Petri net analysis. There are many basic methods to solve it, includingstate equation, T_invariant and reachability graph. The reachability graph corresponds to theusual formal representation of the behavior of the Petri net. However, due to the well-knowncombinatorial explosion problem, it is impossible to exploring the reachability graphexhaustively. Fortunately, it has been shown that the reachability problem is decidable,although it is EXP-TIME and EXP-SPACE hard in the general case.In this thesis, we focus on three types of reachability problem, based on constraintsprogramming and the Logical Abstraction Technique presented by Benasser and Yim. Thesethree reachability problem are defined as follow:(1)Problem 1: "Given a Petri netΣ=(P,T;F,W, m₀) and a final marking m_f,decide if m_f reachable from the initial marking m₀".(2)Problem 2: "Given a Petri netΣ=(P, T; F, W, m₀) and a set of markings, decide ifeach of them reachable from the initial marking m₀".(3)Problem 3: "Given a Petri netΣ=(P,T;F,W, m₀) and a T_vector U, decide if thetransition sequences correspond to the T_vector U is friable from the initial marking m₀; Inother words, decide if the marking m_f=m₀+C.U generated by the T_vector U reachablefrom the initial marking m₀".To solve the problems given above, our works fall into the following aspects:Firstly, after analyzing the characteristic of Logical Abstraction Technique, we define theMaximum Steps set, the Key Markings and the Key Transitions. Then we prove that using theKey Markings and the Key Transitions can exactly capture the concrete steps and markingsexcluding the possibility of identical markings appeared in other partial steps or partialmarkings. (2)Secondly, being supported by our proposition, we propose the Key Constraintsalgorithm, which not only can run efficiently and effectively in the Petri net with multi-tokenand/or repetitive markings (having a cycle in the reachability graph or a different transitionsequences in an identical marking), but also compute the sequential depth parameter ofbounded Petri net by using less additional variables and constrains. What's more, the KeyConstraints algorithm is good at solving the reachability problem of a set of markings definedin Problem 2.(3)Finally, after analyzing some methods of solving the reachability problem defined inProblem 3, we recreate our constraints model and present a new algorithm. The newalgorithm uses the Forward Checking method to avoid searching the paths unrelated T_vectorU. We also consider the constraints search strategy to make our variables rapidly approachesthe target. Our result show that the algorithm is good at Problem 3 with the Petri net havingmulti-token and/or repetitive markings.