Optimal Reachability in Cost Time Petri Nets

In order to model resource-consumption or allocation problems in concurrent real-time systems, we propose an extension of time Petri nets (TPN) with a linear cost function and investigate the minimum/infimum cost reachability problem. We build on the good properties of the state class symbolic abstraction, which is coarse and requires no approximation (or k-extrapolation) to ensure finiteness, and extend this abstraction to symbolically compute the cost of a given sequence of transitions. We show how this can be done, both by using general convex polyhedra, but also using the more efficient Difference Bound Matrix (DBM) data structure. Both techniques can then be used to obtain a symbolic algorithm for minimum cost reachability in bounded time Petri nets with possibly negative costs (provided there are no negative cost cycles). We prove that this algorithm terminates in both cases by proving that it explores only a finite number of extended state classes for bounded TPN, without having to resort to a bounded clock hypothesis, or to an extra approximation/extrapolation operator. All this is implemented in our tool Romeo and we illustrate the usefulness of these results in a case study.