Didier Lime ; Olivier H. Roux ; Charlotte Seidner - Cost Problems for Parametric Time Petri Nets

fi:8464 - Fundamenta Informaticae, December 23, 2021, Volume 183, Issues 1-2: Petri Nets 2019
Cost Problems for Parametric Time Petri Nets

Authors: Didier Lime ; Olivier H. Roux ; Charlotte Seidner

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.


Volume: Volume 183, Issues 1-2: Petri Nets 2019
Published on: December 23, 2021
Accepted on: September 22, 2021
Submitted on: September 9, 2021
Keywords: Computer Science - Formal Languages and Automata Theory


Share

Consultation statistics

This page has been seen 17 times.
This article's PDF has been downloaded 3 times.