Analysis for Reachability Problem of Bounded Petri Net Using Key Constraints Method

In this paper, we propose an efficient reachability analysis of bounded Petri net using constraint programming. By defining the key markings and the key transitions, we adapt the logical abstraction technique proposed by Benasser and Yim for multi-token and repetitive markings Petri net. Using the key markings and the key transitions, we can not only exactly capture the concrete steps and markings excluding the possibility of identical markings appeared in other partial steps or partial markings, but also compute the sequential depth parameter of bounded Petri net. Our results show that we can find the reachability markings and compute sequential depth parameter more effectively and efficiently.