Cost Problems for Parametric Time Petri Nets

• Autorzy: Lime Didiera , Roux Olivier H. , Seidner Charlotte
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Time Petri nets; reachability; parameters; cost; optimality

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 183, nr 1-2
• Strony: 97--123
• Opis fizyczny: Bibliogr. 23 poz., rys.

Twórcy

autor

Lime Didiera

• École Centrale de Nantes, Nantes, France

autor

Roux Olivier H.

• École Centrale de Nantes, Nantes, France.

autor

Seidner Charlotte

• Université de Nantes, Nantes, France

Bibliografia

• [1] Alur R, Henzinger TA, Vardi MY. Parametric Real-time Reasoning. In: ACM Symposium on Theory of Computing. 1993 pp. 592-601. doi:10.1145/167088.167242.
• [2] Alur R, Dill D. A Theory of Timed Automata. Theoretical Computer Science, 1994. 126(2):183-235. doi:10.1016/0304-3975(94)90010-8.
• [3] Hune T, Romijn J, Stoelinga M, Vaandrager F. Linear Parametric Model Checking of Timed Automata. Journal of Logic and Algebraic Programming, 2002. 52-53:183-220.
• [4] Jovanovi´c A, Lime D, Roux OH. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering (TSE), 2015. 41(5):445-461. doi:10.1109/TSE.2014.2357445.
• [5] Alur R, Torre SL, Pappas GJ. Optimal paths in weighted timed automata. Theoretical Computer Science, 2004. 318(3):297 - 322. doi:10.1016/j.tcs.2003.10.038.
• [6] Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, Vaandrager F. Minimum-Cost Reachability for Priced Timed Automata. In: HSCC 2001 Rome, Italy. Springer. ISBN 978-3-540-45351-2, 2001 pp. 147-161. doi:10.1007/3-540-45351-2 15.
• [7] Behrmann G, Larsen KG, Rasmussen JI. Optimal Scheduling Using Priced Timed Automata. SIGMET-RICS Perform. Eval. Rev., 2005. 32(4):34-40. doi:10.1145/1059816.1059823.
• [8] Larsen K, Behrmann G, Brinksma E, Fehnker A, Hune T, Pettersson P, Romijn J. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In: CAV’01, volume 2102 of LNCS. 2001 pp. 493-505. doi:10.1007/3-540-44585-4 47.
• [9] Bouyer P, Colange M, Markey N. Symbolic Optimal Reachability in Weighted Timed Automata. In: CAV’16, volume 9779 of LNCS. Toronto, Canada, 2016 pp. 513-530. doi:10.1007/978-0-387-35608-2 40.
• [10] Abdulla PA, Mayr R. Priced Timed Petri Nets. Logical Methods in Computer Science, 2013. 9(4). doi:10.2168/LMCS-9(4:10)2013.
• [11] Boucheneb H, Lime D, Parquier B, Roux OH, Seidner C. Optimal Reachability in Cost Time Petri Nets. In: FORMATS’17, Berlin, Germany, LNCS. 2017 pp. 58-73. doi:10.1007/978-3-319-65765-3 4.
• [12] Jovanovi´c A. Parametric Verification of Timed Systems. Ph.D. thesis, ´Ecole Centrale Nantes, Nantes, France, 2013.
• [13] Lime D, Roux OH, Seidner C. Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets. In: Donatelli S, Haar S (eds.), 40th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2019), volume 11522 of Lecture Notes in Computer Science. Springer, Aachen, Germany, 2019 pp. 406-425. doi:10.1007/978-3-030-21571-2 22.
• [14] Berthomieu B, Diaz M. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE trans. on soft. eng., 1991. 17(3):259-273.
• [15] B´erard B, Cassez F, Haddad S, Lime D, Roux OH. Comparison of Different Semantics for Time Petri Nets. In: Peled DA, Tsay YK (eds.), 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2005), volume 3707 of Lecture Notes in Computer Science. Springer-Verlag, Taipei, Taiwan, 2005 pp. 293-307. doi:10.1007/11562948 23.
• [16] Minsky M. Computation: Finite and Infinite Machines. Prentice Hall, 1967.
• [17] Berthomieu B, Menasche M. An Enumerative Approach For Analyzing Time Petri Nets. In: IFIP. Elsevier Science Publishers, 1983 pp. 41-46. ID: 10736503.
• [18] Traonouez LM, Lime D, Roux OH. Parametric Model-Checking of Stopwatch Petri Nets. Journal of Universal Computer Science, 2009. 15(17):3273-3304. doi:10.3217/jucs-015-17-3273.
• [19] Schrijver A. Theory of linear and integer programming. John Wiley & Sons, Inc., New York, NY, USA, 1986. ISBN:0-471-90854-1.
• [20] Larsen KG, Pettersson P, Yi W. Model-Checking for Real-Time Systems. In: Fundamentals of Computation Theory, volume 965 of LNCS. 1995 pp. 62-88. doi:10.1007/3-540-60249-6 41.
• [21] Bagnara R, Hill P, Zaffanella E. Not Necessarily Closed Polyhedra and the Double Description Method. Formal Aspects of Computing, 2005. 17:222-257. doi:10.1007/s00165-005-0061-1.
• [22] AUTOSAR. Specification of RTE Software. Technical Report 4.4.0, 2018.
• [23] Naumann N. AUTOSAR Runtime Environment and Virtual Function Bus. Technical report, Hasso-Plattner-Institut, 2009.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)