Using Constraint Programming for solving the Reachability Problem in Timed Petri Nets: Evaluation of Basic Labeling Strategies

In this paper, we propose to use a constraint programming approach to address the reachability problem in Timed Petri Nets (TPNs). TPNs can be used to model a wide class of systems, from manufacturing issues to formal verification of embedded systems. Many of the considered problems can be modeled as reachability problems in TPNs. To reduce the space state explosion brought by the exploration of the TPN behavior, we propose to follow the incremental methodology proposed by Bourdeaud'huy and Hanafi (2006), who translate the reachability graph of Timed PNs into a mathematical model. We improve this model by adding valid inequalities and search for solutions using Constraint Programming (CP). More particularly, we compare different labeling strategies and assess their respective efficiency.