Abstract
Reinforcement Learning (RL) is a powerful technique to control autonomous hybrid systems (HSs) in dynamic and uncertain environments but makes it hard to guarantee their correct behavior in safety-critical applications. To formally guarantee safe behavior, a formal system description is required, which is often not available in industrial design processes and hard to obtain for the unpredictable, trial and error learning processes of RL. In this paper, we present an approach for semi-automatic deductive verification of intelligent HSs with embedded RL components modeled in Simulink together with the RL Toolbox. Our key ideas are threefold: First, we capture the safety-relevant behavior of RL components with hybrid contracts in differential dynamic logic. Second, we verify safety properties of the overall system with the RL component replaced by its contract deductively using the interactive theorem prover KeYmaera X. To make this possible, we precisely capture the semantics of industrially designed intelligent HSs by extending an existing transformation from Simulink to differential dynamic logic to support RL components. Third, we ensure that contracts are complied with at runtime by automatically deriving runtime monitors from our hybrid contracts. We demonstrate the practical applicability, scalability, and flexibility of our approach by verifying collision freedom of an autonomous intelligent robot in a factory setting.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)
Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems properties with theorem proving. In: 2014 UKACC International Conference on Control, CONTROL 2014 - Proceedings, pp. 244–249. IEEE (2014)
Ashok, P., Křetínský, J., Larsen, K.G., Le Coënt, A., Taankvist, J.H., Weininger, M.: SOS: safe, optimal and small strategies for hybrid markov decision processes. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 147–164. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30281-8_9
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17
Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64–75 (2003)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36
Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)
Hartsell, C., et al.: Model-based design for CPS with learning-enabled components. In: Proceedings of the Workshop on Design Automation for CPS and IoT, pp. 1–9. DESTION ’19, Association for Computing Machinery, New York, NY, USA (2019)
Herber, P., Reicherdt, R., Bittner, P.: Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: International Conference on Embedded Software (EMSOFT), pp. 1–10. IEEE (2013)
Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475–478. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_40
Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in simulink with keymaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89–105. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_6
Liebrenz, T., Herber, P., Glesner, S.: A service-oriented approach for decomposing and verifying hybrid system models. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 127–146. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2_7
Minopoli, S., Frehse, G.: SL2SX translator: from simulink to spaceex models. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 93–98. HSCC ’16, Association for Computing Machinery, New York, NY, USA (2016)
Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36(12), 1312–1340 (2017)
Mitsch, S., Platzer, A.: The KeYmaera X Proof IDE - concepts on usability in hybrid systems theorem proving. Electronic Proceedings in Theoretical Computer Science, vol. 240 (2017)
Phan, D., et al.: A component-based simplex architecture for high-assurance cyber-physical systems. In: 2017 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 49–58. IEEE (2017)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)
Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB/Simulink models using boogie. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190–204. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_14
Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, 2nd edn. The MIT Press Cambridge, Massachusetts London, England (2018)
The MathWorks: White Paper: Code Verification and Run-Time Error Detection Through Abstract Interpretation (2008)
The MathWorks: MATLAB Simulink (2021). www.mathworks.com/products/simulink.html
The MathWorks: Reinforcement Learning Toolbox (2021). https://www.mathworks.com/products/reinforcement-learning.html
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Adelt, J., Liebrenz, T., Herber, P. (2021). Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-90870-6_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-90869-0
Online ISBN: 978-3-030-90870-6
eBook Packages: Computer ScienceComputer Science (R0)