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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 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.
References
Angeli, D., Sontag, E.D.: Monotone control systems. IEEE Trans. Autom. Control 48(10), 1684–1698 (2003)
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
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
Bouissou, O., Martel, M.: GRKLib: a guaranteed Runge Kutta library. In: Scientific Computing, Computer Arithmetic and Validated Numerics (2006)
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
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
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)
Donchev, T., Farkhi, E.: Stability and Euler approximation of one-sided Lipschitz differential inclusions. SIAM J. Control Optim. 36(2), 780–796 (1998)
Fribourg, L., Soulat, R.: Control of Switching Systems by Invariance Analysis: Applcation to Power Electronics. Wiley, New York (2013)
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
Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947–953 (2012)
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)
Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)
Kader, Z., Girard, A., Saoud, A.: Symbolic models for incrementally stable switched systems with aperiodic time sampling? IFAC-PapersOnLine 51, 253–258 (2018)
Kido, K., Sedwards, S., Hasuo, I.: Bounding errors due to switching delays in incrementally stable switched systems. IFAC PapersOnLine 51(16), 247–252 (2018)
Kim, E.S., Arcak, M., Seshia, S.A.: Symbolic control design for monotone systems with directed specifications. Automatica 83, 10–19 (2017)
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
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
Le Coënt, A.: Guaranteed control synthesis for switched space-time dynamical systems. Theses, Université Paris Saclay, October 2017
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)
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)
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)
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)
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)
Meyer, P.-J., Girard, A., Witrant, E.: Robust controlled invariance for monotone systems: application to ventilation regulation in buildings. Automatica 70, 14–20 (2016)
Moore, R.: Interval Analysis. Prentice Hall, Upper Saddle River (1966)
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)
Pintér, J.D.: Global Optimization in Action: Continuous and Lipschitz Optimization: Algorithms, Implementations and Applications. Springer, Heidelberg (2013)
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)
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)
Saoud, A., Girard, A., Fribourg, L.: On the composition of discrete and continuous-time assume-guarantee contracts for invariance (2018)
Söderlind, G.: On nonlinear difference and differential equations. BIT Numer. Math. 24(4), 667–680 (1984)
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
Corresponding author
Editor information
Editors and Affiliations
A Uppaal Functions
A Uppaal Functions
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)