Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2018: Formal Methods pp 203–221Cite as

Optimal and Robust Controller Synthesis

Using Energy Timed Automata with Uncertainty

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10951))

Abstract

In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing constraints and variable energy rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.

Work supported by ERC projects Lasso and EQualIS.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    For the infinite-run problem, it can be shown that memoryless strategies suffice.

  2. 2.

    More details on our scripts are available at http://people.cs.aau.dk/~giovbacci/tools.html, together with the models we used for our examples and case study.

References

  1. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  3. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45351-2_8

    Chapter  Google Scholar 

  4. Bacci, G., Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Reynier, P.-A.: Optimal and robust controller synthesis: using energy timed automata with uncertainty (2018). arXiv:1805.00847 [cs.FL]

  5. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_14

    Chapter  Google Scholar 

  6. 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_15

    Chapter  Google Scholar 

  7. Bemporad, A., Ferrari-Trecate, G., Morari, M.: Observability and controllability of piecewise affine and hybrid systems. IEEE Trans. Autom. Control 45(10), 1864–1876 (2000)

    Article  MathSciNet  Google Scholar 

  8. Bisgaard, M.: Battery-aware scheduling in low orbit: the GomX–3 case. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 559–576. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_34

    Chapter  Google Scholar 

  9. Blondel, V.D., Bournez, O., Koiran, P., Tsitsiklis, J.N.: The stability of saturated linear dynamical systems is undecidable. J. Comput. Syst. Sci. 62(3), 442–462 (2001)

    Article  MathSciNet  Google Scholar 

  10. Blondel, V.D., Tsitsiklis, J.N.: Complexity of stability and controllability of elementary hybrid systems. Automatica 35(3), 479–489 (1999)

    Article  MathSciNet  Google Scholar 

  11. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th International Workshop on Hybrid Systems: Computation and Control (HSCC 2010), pp. 61–70. ACM Press, April 2010

    Google Scholar 

  12. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85778-5_4

    Chapter  MATH  Google Scholar 

  13. Bouyer, P., Larsen, K.G., Markey, N.: Lower-bound constrained runs in weighted timed automata. Perform. Eval. 73, 91–109 (2014)

    Article  Google Scholar 

  14. Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006). https://doi.org/10.1007/11787006_49

    Chapter  MATH  Google Scholar 

  15. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452_9

    Chapter  Google Scholar 

  16. Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers – an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 90–104. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00602-9_7

    Chapter  MATH  Google Scholar 

  17. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028751

    Chapter  Google Scholar 

  18. David, A., et al.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129–145. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_10

    Chapter  Google Scholar 

  19. David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_16

    Chapter  Google Scholar 

  20. Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. STTT 10(3), 263–279 (2008)

    Article  MathSciNet  Google Scholar 

  21. Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, 9–14 October 2011, pp. 107–116. ACM (2011)

    Google Scholar 

  22. Markey, N.: Verification of Embedded Systems - Algorithms and Complexity. Mémoire d’habilitation, École Normale Supérieure de Cachan, France (2011)

    Google Scholar 

  23. Miremadi, S., Fei, Z., Åkesson, K., Lennartson, B.: Symbolic supervisory control of timed discrete event systems. IEEE Trans. Contr. Syst. Technol. 23(2), 584–597 (2015)

    Article  Google Scholar 

  24. Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_51

    Chapter  Google Scholar 

  25. Phan, A.-D., Hansen, M.R., Madsen, J.: EHRA: specification and analysis of energy-harvesting wireless sensor networks. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 520–540. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54624-2_26

    Chapter  MATH  Google Scholar 

  26. Quasimodo: Quantitative system properties in model-driven design of embedded systems. http://www.quasimodo.aau.dk/

  27. von Bochmann, G., Hilscher, M., Linker, S., Olderog, E.: Synthesizing and verifying controllers for multi-lane traffic maneuvers. Formal Asp. Comput. 29(4), 583–600 (2017)

    Article  MathSciNet  Google Scholar 

  28. Wolfram Research, Inc.: Mathematica, Version 11.2. Champaign (2017)

    Google Scholar 

  29. Zhao, H., Zhan, N., Kapur, D., Larsen, K.G.: A “hybrid” approach for synthesizing optimal controllers of hybrid systems: a case study of the oil pump industrial example. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 471–485. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_38

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Giovanni Bacci & Kim Guldstrand Larsen

  2. LSV, CNRS & ENS Cachan, Université Paris-Saclay, Cachan, France

    Patricia Bouyer

  3. École Polytechnique, Palaiseau, France

    Uli Fahrenberg

  4. Univ. Rennes, IRISA, CNRS & INRIA, Rennes, France

    Nicolas Markey

  5. Aix Marseille Univ., Université de Toulon, CNRS, LIS, Marseille, France

    Pierre-Alain Reynier

Authors
  1. Giovanni Bacci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Patricia Bouyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Nicolas Markey
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Pierre-Alain Reynier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giovanni Bacci .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bacci, G., Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Reynier, PA. (2018). Optimal and Robust Controller Synthesis. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation