Skip to main content
SpringerLink
Log in

Guaranteed Control Synthesis for Continuous Systems in Uppaal Tiga

  • Conference paper
  • First Online:
Cyber Physical Systems. Model-Based Design (CyPhy 2018, WESE 2018)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 11615))

Abstract

We present a method for synthesising control strategies for continuous dynamical systems. We use Uppaal Tiga for the synthesis in combination with a set-based Euler method for guaranteeing that the synthesis is safe. We present both a general method and a method which provides tighter bounds for monotone systems. As a case-study, we synthesize a guaranteed safe strategy for a simplified adaptive cruise control application. We show that the guaranteed strategy is only slightly more conservative than the strategy generated in the original adaptive cruise control paper which uses a discrete non guaranteed strategy. Also, we show how reinforcement learning may be used to obtain optimal sub-strategies.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    The method described actually calculates a box which is specified using reals, we then round these to obtain integers to make it possible to do the synthesis.

  2. 2.

    In order to obtain a monotone system from the cruise control model, simply right (3) as \(-\dot{v}_e = -a_e\) in order to have an addition in (4) which will indeed verify the monotonicity hypothesis.

References

  1. Angeli, D., Sontag, E.D.: Monotone control systems. IEEE Trans. Autom. Control 48(10), 1684–1698 (2003)

    Article  MathSciNet  Google Scholar 

  2. 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 

  3. Bouissou, O., Chapoutot, A., Djoudi, A.: Enclosing temporal evolution of dynamical systems using numerical methods. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 108–123. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_8

    Chapter  Google Scholar 

  4. Bouissou, O., Martel, M.: GRKLib: a guaranteed Runge Kutta library. In: Scientific Computing, Computer Arithmetic and Validated Numerics (2006)

    Google Scholar 

  5. David, A., Fang, H., Larsen, K.G., Zhang, Z.: Verification and performance evaluation of timed game strategies. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 100–114. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10512-3_8

    Chapter  Google Scholar 

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

  7. David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal stratego. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 206–211. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  8. Donchev, T., Farkhi, E.: Stability and Euler approximation of one-sided Lipschitz differential inclusions. SIAM J. Control Optim. 36(2), 780–796 (1998)

    Article  MathSciNet  Google Scholar 

  9. Fribourg, L., Soulat, R.: Control of Switching Systems by Invariance Analysis: Applcation to Power Electronics. Wiley, New York (2013)

    Book  Google Scholar 

  10. Gajda, K., Jankowska, M., Marciniak, A., Szyszka, B.: A survey of interval Runge–Kutta and multistep methods for solving the initial value problem. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Wasniewski, J. (eds.) PPAM 2007. LNCS, vol. 4967, pp. 1361–1371. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68111-3_144

    Chapter  Google Scholar 

  11. Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947–953 (2012)

    Article  MathSciNet  Google Scholar 

  12. Girard, A., Martin, S.: Synthesis for constrained nonlinear systems using hybridization and robust controllers on simplices. IEEE Trans. Autom. Control 57(4), 1046–1051 (2012)

    Article  MathSciNet  Google Scholar 

  13. Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)

    Article  MathSciNet  Google Scholar 

  14. Kader, Z., Girard, A., Saoud, A.: Symbolic models for incrementally stable switched systems with aperiodic time sampling? IFAC-PapersOnLine 51, 253–258 (2018)

    Article  Google Scholar 

  15. Kido, K., Sedwards, S., Hasuo, I.: Bounding errors due to switching delays in incrementally stable switched systems. IFAC PapersOnLine 51(16), 247–252 (2018)

    Article  Google Scholar 

  16. Kim, E.S., Arcak, M., Seshia, S.A.: Symbolic control design for monotone systems with directed specifications. Automatica 83, 10–19 (2017)

    Article  MathSciNet  Google Scholar 

  17. Larsen, K.G., Mikučionis, M., Muñiz, M., Srba, J., Taankvist, J.H.: Online and compositional learning of controllers with application to floor heating. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 244–259. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_14

    Chapter  Google Scholar 

  18. Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Safe and optimal adaptive cruise control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 260–277. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23506-6_17

    Chapter  Google Scholar 

  19. Le Coënt, A.: Guaranteed control synthesis for switched space-time dynamical systems. Theses, Université Paris Saclay, October 2017

    Google Scholar 

  20. Coënt, A.L., De Vuyst, F., Chamoin, L., Fribourg, L.: Control synthesis of nonlinear sampled switched systems using Euler’s method. In: Ábrahám, E., Bogomolov, S. (eds.) Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, Uppsala, Sweden, 22nd April 2017. Electronic Proceedings in Theoretical Computer Science, vol. 247, pp. 18–33. Open Publishing Association (2017)

    Google Scholar 

  21. Le Coënt, A., Chapoutot, A., Fribourg, L., Alexandre dit Sandretto, J.A.: An improved algorithm for the control synthesis of nonlinear sampled switched systems. Formal Methods Syst. Des. 53(3), 1–21 (2017)

    MATH  Google Scholar 

  22. Le Coënt, A., Fribourg, L., Markey, N., De Vuyst, F., Chamoin, L.: Compositional synthesis of state-dependent switching control. Theor. Comput. Sci. 750, 53–68 (2018)

    Article  MathSciNet  Google Scholar 

  23. Lin, H., Antsaklis, P.J.: Stability and stabilizability of switched linear systems: a survey of recent results. IEEE Trans. Autom. control 54(2), 308–322 (2009)

    Article  MathSciNet  Google Scholar 

  24. Meyer, P.-J., Girard, A., Witrant, E.: Safety control with performance guarantees of cooperative systems using compositional abstractions. IFAC PapersOnLine 48(27), 317–322 (2015)

    Article  Google Scholar 

  25. Meyer, P.-J., Girard, A., Witrant, E.: Robust controlled invariance for monotone systems: application to ventilation regulation in buildings. Automatica 70, 14–20 (2016)

    Article  MathSciNet  Google Scholar 

  26. Moore, R.: Interval Analysis. Prentice Hall, Upper Saddle River (1966)

    Google Scholar 

  27. Nedialko, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comput. 105(1), 21–68 (1999)

    MathSciNet  MATH  Google Scholar 

  28. Pintér, J.D.: Global Optimization in Action: Continuous and Lipschitz Optimization: Algorithms, Implementations and Applications. Springer, Heidelberg (2013)

    Google Scholar 

  29. Rungger, M., Zamani, M.: SCOTS: a tool for the synthesis of symbolic controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 99–104. ACM, New York (2016)

    Google Scholar 

  30. Saoud, A., Girard, A., Fribourg, L.: Contract based design of symbolic controllers for vehicle platooning. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), pp. 277–278. ACM, New York (2018)

    Google Scholar 

  31. Saoud, A., Girard, A., Fribourg, L.: On the composition of discrete and continuous-time assume-guarantee contracts for invariance (2018)

    Google Scholar 

  32. Söderlind, G.: On nonlinear difference and differential equations. BIT Numer. Math. 24(4), 667–680 (1984)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

This work is supported by the LASSO project financed by an ERC adv. grant; the DiCyPS project funded by Innovation Fund Denmark; and the Eurostars project Reachi.

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, 9220, Aalborg Øst, Denmark

    Kim Guldstrand Larsen, Adrien Le Coënt, Marius Mikučionis & Jakob Haahr Taankvist

Authors
  1. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adrien Le Coënt
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marius Mikučionis
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jakob Haahr Taankvist
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adrien Le Coënt .

Editor information

Editors and Affiliations

  1. Computer Science and Engineering, Washington University, St. Louis, MO, USA

    Roger Chamberlain

  2. School of Information Technology, Halmstad University, Halmstad, Sweden

    Walid Taha

  3. Department of Machine Design, KTH Royal Institute of Technology, Stockholm, Sweden

    Martin Törngren

A Uppaal Functions

A Uppaal Functions

figure h
figure i

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Larsen, K.G., Le Coënt, A., Mikučionis, M., Taankvist, J.H. (2019). Guaranteed Control Synthesis for Continuous Systems in Uppaal Tiga. In: Chamberlain, R., Taha, W., Törngren, M. (eds) Cyber Physical Systems. Model-Based Design. CyPhy WESE 2018 2018. Lecture Notes in Computer Science(), vol 11615. Springer, Cham. https://doi.org/10.1007/978-3-030-23703-5_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-23703-5_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-23702-8

  • Online ISBN: 978-3-030-23703-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation