{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T23:24:45Z","timestamp":1756682685762,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031606977"},{"type":"electronic","value":"9783031606984"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_16","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"279-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Validation of\u00a0Reinforcement Learning Agents and\u00a0Safety Shields with\u00a0ProB"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2556-5553","authenticated-orcid":false,"given":"Fabian","family":"Vu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881","DOI":"10.1017\/CBO9781139195881"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R., Hoare, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005). https:\/\/doi.org\/10.1017\/CBO9780511624162","DOI":"10.1017\/CBO9780511624162"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Form. Methods Syst. Des. 54(3), 416\u2013448 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00333-0","DOI":"10.1007\/s10703-019-00333-0"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings AAAI, pp. 2669\u20132678. AAAI Press (2018). https:\/\/doi.org\/10.1609\/aaai.v32i1.11797","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-030-85248-1_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Bendisposto","year":"2021","unstructured":"Bendisposto, J., et al.: ProB2-UI: a java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193\u2013201. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_12"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Proceedings AAAI, pp. 6485\u20136492. AAAI Press (2018). https:\/\/doi.org\/10.1609\/aaai.v32i1.12107","DOI":"10.1609\/aaai.v32i1.12107"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 3\u201318. IEEE (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Huang, X., Ruan, W., Tang, Q., Zhao, X.: Bridging formal methods and machine learning with global optimisation. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering. ICFEM 2022. LNCS, vol. 13478, pp. 1\u201319. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_1","DOI":"10.1007\/978-3-031-17244-1_1"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, T., Bondu, M., Ishikawa, F.: Formal modelling of safety architecture for responsibility-aware autonomous vehicle via event-b refinement. In: Proceedings FM\u20192023, pp. 533\u2013549 (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_30","DOI":"10.1007\/978-3-031-27481-7_30"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-030-61362-4_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B K\u00f6nighofer","year":"2020","unstructured":"K\u00f6nighofer, B., Lorber, F., Jansen, N., Bloem, R.: Shield synthesis for reinforcement learning. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 290\u2013306. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_16"},{"key":"16_CR13","unstructured":"Krings, S.: Towards Infinite-State Symbolic Model Checking for B and Event-B. Ph.D. thesis, Heinrich Heine Universit\u00e4t D\u00fcsseldorf, August 2017"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Landers, M., Doryab, A.: Deep reinforcement learning verification: a survey. ACM Comput. Surv. 55(14s) (2023). https:\/\/doi.org\/10.1145\/3596444","DOI":"10.1145\/3596444"},{"key":"16_CR15","unstructured":"Leurent, E.: An Environment for Autonomous Driving Decision-Making (2018). https:\/\/github.com\/eleurent\/highway-env"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0063-9","DOI":"10.1007\/s10009-007-0063-9"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning Markov decision processes for model checking. In: Proceedings QFM, pp. 49\u201363. EPTCS 103, Open Publishing Association (2012). http:\/\/dx.doi.org\/10.4204\/EPTCS.103.6","DOI":"10.4204\/EPTCS.103.6"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255\u2013299 (2016). https:\/\/doi.org\/10.1007\/s10994-016-5565-9","DOI":"10.1007\/s10994-016-5565-9"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Mnih, V., et\u00a0al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529\u2013533 (2015). https:\/\/doi.org\/10.1038\/nature14236","DOI":"10.1038\/nature14236"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Peer, E., Menkovski, V., Zhang, Y., Lee, W.J.: Shunting trains with deep reinforcement learning. In: Proceedings SMC, pp. 3063\u20133068. IEEE (2018). https:\/\/doi.org\/10.1109\/SMC.2018.00520","DOI":"10.1109\/SMC.2018.00520"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-55754-6_6","volume-title":"NASA Formal Methods","author":"DT Phan","year":"2020","unstructured":"Phan, D.T., Grosu, R., Jansen, N., Paoletti, N., Smolka, S.A., Stoller, S.D.: Neural simplex architecture. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 97\u2013114. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_6"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 12(1), 9\u201321 (2010). https:\/\/doi.org\/10.1007\/s10009-009-0132-3","DOI":"10.1007\/s10009-009-0132-3"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Razzaghi, P., et al.: A Survey on Reinforcement Learning in Aviation Applications (2022). https:\/\/doi.org\/10.48550\/arXiv.2211.02147","DOI":"10.48550\/arXiv.2211.02147"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: Proceedings IJCAI, pp. 2651\u20132659 (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/368","DOI":"10.24963\/ijcai.2018\/368"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Rudin, C.: Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nat. Mach. Intell. 1(5), 206\u2013215 (2019). https:\/\/doi.org\/10.1038\/s42256-019-0048-x","DOI":"10.1038\/s42256-019-0048-x"},{"issue":"19","key":"16_CR27","doi-asserted-by":"publisher","first-page":"70","DOI":"10.2352\/ISSN.2470-1173.2017.19.AVM-023","volume":"29","author":"A Sallab","year":"2017","unstructured":"Sallab, A., Abdou, M., Perot, E., Yogamani, S.: Deep reinforcement learning framework for autonomous driving. Electron. Imaging 29(19), 70\u201376 (2017). https:\/\/doi.org\/10.2352\/ISSN.2470-1173.2017.19.AVM-023","journal-title":"Electron. Imaging"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46\u201355 (2022). https:\/\/doi.org\/10.1145\/3503914","DOI":"10.1145\/3503914"},{"issue":"4","key":"16_CR29","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/MS.2001.936213","volume":"18","author":"L Sha","year":"2001","unstructured":"Sha, L.: Using simplicity to control complexity. IEEE Softw. 18(4), 20\u201328 (2001). https:\/\/doi.org\/10.1109\/MS.2001.936213","journal-title":"IEEE Softw."},{"key":"16_CR30","unstructured":"Shalev-Shwartz, S., Shammah, S., Shashua, A.: On a formal model of safe and scalable self-driving cars. CoRR abs\/1708.06374 (2017). http:\/\/arxiv.org\/abs\/1708.06374"},{"key":"16_CR31","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (2018)"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Tappler, M., Aichernig, B.K.: Differential safety testing of deep RL agents enabled by automata learning. In: Steffen, B. (eds.) Bridging the Gap Between AI and Reality. AISoLA 2023. LNCS, vol. 14380, pp. 138\u2013159 Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_8","DOI":"10.1007\/978-3-031-46002-9_8"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Tappler, M., Cano Cordoba, F., Aichernig, B., K\u00f6nighofer, B.: Search-based testing of reinforcement learning. In: Proceedings IJCAI, pp. 503\u2013510 (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/72","DOI":"10.24963\/ijcai.2022\/72"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Cai, F., Diego, M.L., Musau, P., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201322 (2019). https:\/\/doi.org\/10.1145\/3358230","DOI":"10.1145\/3358230"},{"issue":"5","key":"16_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527448","volume":"55","author":"GA Vouros","year":"2022","unstructured":"Vouros, G.A.: Explainable deep reinforcement learning: state of the art and challenges. ACM Comput. Surv. 55(5), 1\u201339 (2022). https:\/\/doi.org\/10.1145\/3527448","journal-title":"ACM Comput. Surv."},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Vu, F., Happe, C., Leuschel, M.: Generating interactive documents for domain-specific validation of formal models. STTT (2024). https:\/\/doi.org\/10.1007\/s10009-024-00739-0","DOI":"10.1007\/s10009-024-00739-0"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-031-33163-3_5","volume-title":"Rigorous State-Based Methods","author":"F Vu","year":"2023","unstructured":"Vu, F., Leuschel, M.: Validation of\u00a0formal models by\u00a0interactive simulation. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 59\u201369. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_5"},{"key":"16_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-77543-8_6","volume-title":"Rigorous State-Based Methods","author":"F Vu","year":"2021","unstructured":"Vu, F., Leuschel, M., Mashkoor, A.: Validation of formal models by timed probabilistic simulation. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 81\u201396. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_6"},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"Wang, X., Nair, S., Althoff, M.: Falsification-based robust adversarial reinforcement learning. In: Proceedings ICMLA, pp. 205\u2013212. IEEE (2020). https:\/\/doi.org\/10.1109\/ICMLA51294.2020.00042","DOI":"10.1109\/ICMLA51294.2020.00042"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Watkins, C.J., Dayan, P.: Q-learning. Mach. Learn. 8, 279\u2013292 (1992). https:\/\/doi.org\/10.1007\/BF00992698","DOI":"10.1007\/BF00992698"},{"key":"16_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-030-48077-6_21","volume-title":"Rigorous State-Based Methods","author":"M Werth","year":"2020","unstructured":"Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 260\u2013265. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_21"},{"key":"16_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-1967-3","volume-title":"Machine Learning","author":"Z-H Zhou","year":"2021","unstructured":"Zhou, Z.-H.: Machine Learning. Springer, Singapore (2021). https:\/\/doi.org\/10.1007\/978-981-15-1967-3"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:04:08Z","timestamp":1716768248000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}