nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets

verfasst von : Didier Lime, Olivier H. Roux, Charlotte Seidner

Erschienen in: Application and Theory of Petri Nets and Concurrency

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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 the cost variable stays within a given budget.

We first prove that the mere existence of such values for the parameters is undecidable. We nonetheless provide a symbolic semi-algorithm that is proved both sound and complete when it terminates. We also show how to modify it for the case when parameters values are integers. Finally, we prove that this modified version terminates if parameters are bounded. While this is to be expected since there are now only a finite number of possible parameter values, this is interesting because the computation is symbolic and thus avoids an explicit enumeration of all those values. Furthermore, the result is a symbolic constraint representing a finite union of convex polyhedra that is 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 hybrid extensions of time Petri nets.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel The Combinatorics of Barrier Synchronization

Nächstes Kapitel Coverability and Termination in Recursive Petri Nets

Every 200 t.u., since T1 is executed twice as often as T2, T1 is running during \((22+a)*2=44+2a\) t.u. whereas T2 is running during \(28+(76-2a)=104-2a\) t.u.

To ensure a correct access to the cores, we could have added one place for each core and some arcs on each task to capture and release them but the resulting net would have been quite unreadable. Instead, we chose to add 2 integer variables C0 and C1 (both initialised to 0); a variable equal to 0 (resp. 1) obviously means the corresponding core is idle (resp. busy).

The last term ensures that such cases where an instance of a task is activated while a previous one is running are heavily penalised.

Abdulla, P.A., Mayr, R.: Priced timed Petri nets. Log. Meth. Comput. Sci. 9(4) (2013)

Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRef

Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM Symposium on Theory of Computing, pp. 592–601 (1993)

Alur, R., Torre, S.L., Pappas, G.J.: Optimal paths in weighted timed automata. Theor. Comput. Sci. 318(3), 297–322 (2004)MathSciNetCrossRef

AUTOSAR: specification of RTE software. Technical report 4.4.0, October 2018

Bagnara, R., Hill, P., Zaffanella, E.: Not necessarily closed polyhedra and the double description method. Form. Asp. Comput. 17, 222–257 (2005)CrossRef

Behrmann, G., et al.: Minimum-cost reachability for priced time automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45351-2_15CrossRef

Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. SIGMETRICS Perform. Eval. Rev. 32(4), 34–40 (2005)CrossRef

Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Soft. Eng. 17(3), 259–273 (1991)MathSciNetCrossRef

10.

Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: IFIP, pp. 41–46. Elsevier Science Publishers (1983)

11.

Boucheneb, H., Lime, D., Parquier, B., Roux, O.H., Seidner, C.: Optimal reachability in cost time Petri nets. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 58–73. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_4CrossRef

12.

Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 513–530. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_28CrossRef

13.

Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52–53, 183–220 (2002)MathSciNetCrossRef

14.

Jovanović, A.: Parametric verification of timed systems. Ph.D. thesis, École Centrale Nantes, Nantes, France (2013)

15.

Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. (TSE) 41(5), 445–461 (2015)CrossRef

16.

Larsen, K., et al.: As cheap as possible: effcient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_47CrossRef

17.

Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60249-6_41CrossRef

18.

Minsky, M.: Computation: Finite and Infinite Machines. Prentice Hall, Englewood Cliffs (1967)MATH

19.

Naumann, N.: AUTOSAR runtime environment and virtual function bus. Technical report, Hasso-Plattner-Institut (2009)

20.

Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)MATH

21.

Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univers. Comput. Sci. 15(17), 3273–3304 (2009)MathSciNetMATH

Titel: Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
verfasst von: Didier Lime
Olivier H. Roux
Charlotte Seidner
Verlag: Springer International Publishing
Buch: Application and Theory of Petri Nets and Concurrency
Print ISBN: 978-3-030-21570-5

Electronic ISBN: 978-3-030-21571-2

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-21571-2_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"