Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Termination Analysis of Probabilistic Programs Through Positivstellensatz’s Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Symbolic Optimal Reachability in Weighted Timed Automata

Authors : Patricia Bouyer, Maximilien Colange, Nicolas Markey

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Weighted timed automata have been defined in the early 2000 s for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Counterexample Guided Abstraction Refinement for Stability Analysis
next chapter Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
Footnotes
1
Contrary to pure reachability, we cannot use the preorder \(\preceq _{LU}\) (which distinguishes between lower-bounded constraints and upper-bounded constraints) [BBLP06], since it does not preserve optimal cost (not even optimal time).
 
Literature
[ACHH93]
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1993. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)CrossRef
[AD90]
Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRef
[AD94]
[AFM+03]
Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, Kim Guldstrand, Niebert, Peter (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)CrossRef
[ALP01]
Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)CrossRef
[ARF14]
Al-Bataineh, O., Reynolds, M., French, T.: Finding best and worst case execution times of systems using difference-bound matrices. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 38–52. Springer, Heidelberg (2014)
[BBBR07]
Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem. Form. Methods Syst. Des. 31(2), 135–175 (2007)CrossRefMATH
[BBFL03]
Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)CrossRef
[BBL08]
Patricia, B., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Form. Methods Syst. Des. 32(1), 2–23 (2008)MATH
[BBLP06]
Behrmann, G., Bouyer, P., Larsen, K.G., Pelànek, R.: Zone based abstractions for timed automata exploiting lower and upper bounds. Int. J. Softw. Tools Technol. Transf. 8(3), 204–215 (2006)CrossRefMATH
[BCM16]
[BFH+01]
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)CrossRef
[BFLM11]
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Commun. ACM 54(9), 78–87 (2011)CrossRef
[BLR05]
Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. ACM Sigmetrics Perform. Eval. Rev. 32(4), 34–40 (2005)CrossRef
[Bou04]
[BV04]
Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004)CrossRefMATH
[BY03]
Bengtsson, J.E., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491–503. Springer, Heidelberg (2003)CrossRef
[DHS+14]
[DOT+10]
Dalsgaard, A.E., Chr, M., Olesen, M.T., Hansen, R.R., Larsen, K.G.: METAMOC: modular execution time analysis using model checking. In: Proceedings of 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). OpenAccess Series in Informatics (OASIcs), vol. 15, pp. 113–123. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)
[GELP10]
Gustavsson, A., Ermedahl, A., Lisper, B., Pettersson, P.: Towards WCET analysis of multicore architectures using UPPAAL. In: Proceedings of 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). OpenAccess Series in Informatics (OASIcs), vol. 15, pp. 101–112. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)
[HKPV98]
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRefMATH
[HKSW11]
Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: Proceedings of 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). LIPIcs, vol. 13, pp. 78–89. Leibniz-Zentrum für Informatik (2011)
[HSW12]
Frédéric Herbreteau, B., Srivathsan, I.W.: Better abstractions for timed automata. In: Proceedings of 27th Annual Symposium on Logic in Computer Science (LICS 2012), pp. 375–384. IEEE Computer Society Press (2012)
[HT15]
Herbreteau, F., Tran, T.-T.: Improving search order for reachability testing in timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 124–139. Springer, Heidelberg (2015)CrossRef
[JR11]
Jaubert, R., Reynier, P.-A.: Quantitative robustness analysis of flat timed automata. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 229–244. Springer, Heidelberg (2011)CrossRef
[LBB+01]
Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.M.T.: As cheap as possible: efficient 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)CrossRef
[RLS06]
Rasmussen, J.I., Larsen, K.G., Subramani, K.: On using priced timed automata to achieve optimal scheduling. Form. Methods Syst. Des. 29(1), 97–114 (2006)CrossRefMATH
[RS01]
Rückmann, J.-J., Stein, O.: On linear and linearized generalized semi-infinite optimization problem. Ann. Oper. Res. 101(1–4), 191–208 (2001)MathSciNetCrossRefMATH
Metadata
Title
Symbolic Optimal Reachability in Weighted Timed Automata
Authors
Patricia Bouyer
Maximilien Colange
Nicolas Markey
Copyright Year
2016
Book
Computer Aided Verification

Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-41528-4_28

Premium Partner

    Image Credits