Cost Problems for Parametric Time Petri Nets

TL;DR

This paper studies parameter synthesis in cost-augmented time Petri nets, proving undecidability of some problems, and providing symbolic semi-algorithms for cost optimization and reachability, with implementation in the Romeo tool.

Contribution

It introduces symbolic semi-algorithms for parameter synthesis in cost-time Petri nets, handling both continuous and discrete costs, and extends to bounded integer parameters with termination guarantees.

Findings

Existence of suitable parameters is undecidable.

Semi-algorithms are sound and complete when they terminate.

Algorithms produce symbolic constraints for further analysis.

Abstract

We investigate the problem of parameter synthesis for time Petri nets with a cost variable that evolves both continuously with time, and discretely when firing transitions. More precisely, parameters are rational symbolic constants used for time constraints on the firing of transitions and we want to synthesise all their values such that some marking is reachable, with a cost that is either minimal or simply less than a given bound. We first prove that the mere existence of values for the parameters such that the latter property holds is undecidable. We nonetheless provide symbolic semi-algorithms for the two synthesis problems and we prove them both sound and complete when they terminate. We also show how to modify them for the case when parameter values are integers. Finally, we prove that these modified versions terminate if parameters are bounded. While this is to be expected since there are now only a finite number of possible parameter values, our algorithms are symbolic and thus avoid an explicit enumeration of all those values. Furthermore, the results are symbolic constraints representing finite unions of convex polyhedra that are easily amenable to further analysis through linear programming. We finally report on the implementation of the approach in Romeo, a software tool for the analysis of time Petri nets.