{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:49Z","timestamp":1750309609781,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"MARS Project","award":["101091783"],"award-info":[{"award-number":["101091783"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1145\/3672608.3707759","type":"proceedings-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:26:21Z","timestamp":1747247181000},"page":"1514-1521","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["PCTL Model Checking for Temporal RL Policy Safety Explanations"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-5734-0538","authenticated-orcid":false,"given":"Dennis","family":"Gross","sequence":"first","affiliation":[{"name":"Simula Research Laboratory, Oslo, Norway"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2494-4279","authenticated-orcid":false,"given":"Helge","family":"Spieker","sequence":"additional","affiliation":[{"name":"Simula Research Laboratory, Oslo, Norway"}]}],"member":"320","published-online":{"date-parts":[[2025,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. PRISM Manual. http:\/\/www.prismmodelchecker.org\/manual\/"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2024.104182"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2017.2743240"},{"volume-title":"Principles of model checking","author":"Baier Christel","key":"e_1_3_2_1_4_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-023-06479-7"},{"key":"e_1_3_2_1_6_1","unstructured":"David Bertoin Adil Zouitine Mehdi Zouitine and Emmanuel Rachelson. 2022. Look where you look! Saliency-guided Q-networks for generalization in visual Reinforcement Learning. In NeurIPS."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Kayla Boggess Sarit Kraus and Lu Feng. 2023. Explainable Multi-Agent Reinforcement Learning for Temporal Queries. In IJCAI. ijcai.org 55\u201363.","DOI":"10.24963\/ijcai.2023\/7"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"e_1_3_2_1_9_1","volume-title":"Kim Guldstrand Larsen, and Didier Lime","author":"Cassez Franck","year":"2005","unstructured":"Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. 2005. Efficient On-the-Fly Algorithms for the Analysis of Timed Games. In CONCUR (Lecture Notes in Computer Science, Vol. 3653). Springer, 66\u201380."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence (Proceedings of Machine Learning Research","volume":"343","author":"Corsi Davide","year":"2021","unstructured":"Davide Corsi, Enrico Marchesini, and Alessandro Farinelli. 2021. Formal verification of neural networks for safety-critical tasks in deep reinforcement learning. In Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence (Proceedings of Machine Learning Research, Vol. 161), Cassio de Campos and Marloes H. Maathuis (Eds.). PMLR, 333\u2013343. https:\/\/proceedings.mlr.press\/v161\/corsi21a.html"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cor.2023.106521"},{"key":"e_1_3_2_1_12_1","volume-title":"Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist.","author":"David Alexandre","year":"2015","unstructured":"Alexandre David, Peter Gj\u00f8l Jensen, Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist. 2015. Uppaal Stratego. In TACAS (Lecture Notes in Computer Science, Vol. 9035). Springer, 206\u2013211."},{"key":"e_1_3_2_1_13_1","volume-title":"Permissive Controller Synthesis for Probabilistic Systems. Log. Methods Comput. Sci. 11, 2","author":"Dr\u00e4ger Klaus","year":"2015","unstructured":"Klaus Dr\u00e4ger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma. 2015. Permissive Controller Synthesis for Probabilistic Systems. Log. Methods Comput. Sci. 11, 2 (2015)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Tomer Eliyahu Yafim Kazak Guy Katz and Michael Schapira. 2021. Verifying learning-augmented systems. In SIGCOMM. ACM 305\u2013318.","DOI":"10.1145\/3452296.3472936"},{"key":"e_1_3_2_1_15_1","volume-title":"Julieta Noguez, and Alberto Reyes.","author":"Elizalde Francisco","year":"2009","unstructured":"Francisco Elizalde, Luis Enrique Sucar, Julieta Noguez, and Alberto Reyes. 2009. Generating Explanations Based on Markov Decision Processes. In MICAI (Lecture Notes in Computer Science, Vol. 5845). Springer, 51\u201362."},{"volume-title":"ECCV (21) (Lecture Notes in Computer Science","author":"Ganjdanesh Alireza","key":"e_1_3_2_1_17_1","unstructured":"Alireza Ganjdanesh, Shangqian Gao, and Heng Huang. 2022. Interpretations Steered Network Pruning via Amortized Inferred Saliency Maps. In ECCV (21) (Lecture Notes in Computer Science, Vol. 13681). Springer, 278\u2013296."},{"volume-title":"CAV (2) (Lecture Notes in Computer Science","author":"Gros Timo P.","key":"e_1_3_2_1_18_1","unstructured":"Timo P. Gros, Holger Hermanns, J\u00f6rg Hoffmann, Michaela Klauck, Maximilian A. K\u00f6hl, and Verena Wolf. 2022. MoGym: Using Formal Models for Training and Verifying Decision-making Agents. In CAV (2) (Lecture Notes in Computer Science, Vol. 13372). Springer, 430\u2013443."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50086-3_6"},{"key":"e_1_3_2_1_20_1","volume-title":"P\u00e9rez","author":"Gross Dennis","year":"2022","unstructured":"Dennis Gross, Nils Jansen, Sebastian Junges, and Guillermo A. P\u00e9rez. 2022. COOLMC: A Comprehensive Tool for Reinforcement Learning and Model Checking. In SETTA (Lecture Notes in Computer Science, Vol. 13649). Springer, 41\u201349."},{"key":"e_1_3_2_1_21_1","volume-title":"P\u00e9rez","author":"Gross Dennis","year":"2022","unstructured":"Dennis Gross, Nils Jansen, Sebastian Junges, and Guillermo A. P\u00e9rez. 2022. COOLMC: A Comprehensive Tool for Reinforcement Learning and Model Checking. In SETTA. Springer."},{"key":"e_1_3_2_1_22_1","volume-title":"P\u00e9rez","author":"Gross Dennis","year":"2023","unstructured":"Dennis Gross, Christoph Schmidl, Nils Jansen, and Guillermo A. P\u00e9rez. 2023. Model Checking for Adversarial Multi-Agent Reinforcement Learning with Reactive Defense Methods. In ICAPS. AAAI Press, 162\u2013170."},{"key":"e_1_3_2_1_23_1","volume-title":"P\u00e9rez","author":"Gross Dennis","year":"2023","unstructured":"Dennis Gross, Thiago D. Sim\u00e3o, Nils Jansen, and Guillermo A. P\u00e9rez. 2023. Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking. In ICAART (3). SCITEPRESS, 501\u2013508."},{"key":"e_1_3_2_1_24_1","volume-title":"Enhancing RL Safety with Counterfactual LLM Reasoning. arXiv preprint arXiv:2409.10188","author":"Gross Dennis","year":"2024","unstructured":"Dennis Gross and Helge Spieker. 2024. Enhancing RL Safety with Counterfactual LLM Reasoning. arXiv preprint arXiv:2409.10188 (2024)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.14428\/esann\/2024.ES2024-71"},{"volume-title":"TACAS (1) (LNCS","author":"Hahn Ernst Moritz","key":"e_1_3_2_1_26_1","unstructured":"Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. 2019. Omega-Regular Objectives in Model-Free Reinforcement Learning. In TACAS (1) (LNCS, Vol. 11427). Springer, 395\u2013412."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57628-8_1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.3390\/en9100767"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2018.8593649"},{"volume-title":"Efficient LTL Model Checking of Deep Reinforcement Learning Systems using Policy Extraction","author":"Jin Peng","key":"e_1_3_2_1_32_1","unstructured":"Peng Jin, Yang Wang, and Min Zhang. 2022. Efficient LTL Model Checking of Deep Reinforcement Learning Systems using Policy Extraction. In SEKE. KSI Research Inc., 357\u2013362."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Yafim Kazak Clark W. Barrett Guy Katz and Michael Schapira. 2019. Verifying Deep-RL-Driven Systems. In NetAI@SIGCOMM. ACM 83\u201389.","DOI":"10.1145\/3341216.3342218"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3616864"},{"key":"e_1_3_2_1_35_1","volume-title":"Explainable Reinforcement Learning: A Survey and Comparative Review. ACM Comput. Surv. 56, 7","author":"Milani Stephanie","year":"2024","unstructured":"Stephanie Milani, Nicholay Topin, Manuela Veloso, and Fei Fang. 2024. Explainable Reinforcement Learning: A Survey and Comparative Review. ACM Comput. Surv. 56, 7 (2024), 168:1\u2013168:36."},{"key":"e_1_3_2_1_36_1","volume-title":"Riedmiller","author":"Mnih Volodymyr","year":"2013","unstructured":"Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin A. Riedmiller. 2013. Playing Atari with Deep Reinforcement Learning. CoRR abs\/1312.5602 (2013)."},{"key":"e_1_3_2_1_37_1","volume-title":"Human-level control through deep reinforcement learning. Nat. 518, 7540","author":"Mnih Volodymyr","year":"2015","unstructured":"Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G. Bellemare, Alex Graves, Martin A. Riedmiller, Andreas Fidjeland, Georg Ostrovski, Stig Petersen, Charles Beattie, Amir Sadik, Ioannis Antonoglou, Helen King, Dharshan Kumaran, Daan Wierstra, Shane Legg, and Demis Hassabis. 2015. Human-level control through deep reinforcement learning. Nat. 518, 7540 (2015), 529\u2013533."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10015-022-00846-8"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Qi Pang Yuanyuan Yuan and Shuai Wang. 2022. MDPFuzz: testing models solving Markov decision processes. In ISSTA. ACM 378\u2013390.","DOI":"10.1145\/3533767.3534388"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPAMI.2021.3133717"},{"volume-title":"Explaining Deep Reinforcement Learning Agents in the Atari Domain through a Surrogate Model","author":"Sieusahai Alexander","key":"e_1_3_2_1_41_1","unstructured":"Alexander Sieusahai and Matthew Guzdial. 2021. Explaining Deep Reinforcement Learning Agents in the Atari Domain through a Surrogate Model. In AIIDE. AAAI Press, 82\u201390."},{"key":"e_1_3_2_1_42_1","volume-title":"Patrick Ferber, Timo P. Gros, Philippe Heim, Daniel H\u00f6ller, Xandra Schuler, Valentin W\u00fcstholz, Maria Christakis, and J\u00f6rg Hoffmann.","author":"Steinmetz Marcel","year":"2022","unstructured":"Marcel Steinmetz, Daniel Fiser, Hasan Ferit Eniser, Patrick Ferber, Timo P. Gros, Philippe Heim, Daniel H\u00f6ller, Xandra Schuler, Valentin W\u00fcstholz, Maria Christakis, and J\u00f6rg Hoffmann. 2022. Debugging a Policy: Automatic Action-Policy Testing in AI Planning. In ICAPS. AAAI Press, 353\u2013361."},{"key":"e_1_3_2_1_43_1","volume-title":"Littman","author":"Strehl Alexander L.","year":"2007","unstructured":"Alexander L. Strehl, Carlos Diuk, and Michael L. Littman. 2007. Efficient Structure Learning in Factored-State MDPs. In AAAI. AAAI Press, 645\u2013650."},{"volume-title":"Reinforcement learning: An introduction","author":"Sutton Richard S","key":"e_1_3_2_1_44_1","unstructured":"Richard S Sutton and Andrew G Barto. 2018. Reinforcement learning: An introduction. MIT press."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88708-7_19"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.engappai.2024.108553"},{"key":"e_1_3_2_1_47_1","volume-title":"Taylor","author":"Torrey Lisa","year":"2013","unstructured":"Lisa Torrey and Matthew E. Taylor. 2013. Teaching on a budget: agents advising agents in reinforcement learning. In AAMAS. IFAAMAS, 1053\u20131060."},{"key":"e_1_3_2_1_48_1","first-page":"41","article-title":"Scalar reward is not enough: a response to Silver, Singh, Precup and Sutton (2021)","volume":"36","author":"Vamplew Peter","year":"2022","unstructured":"Peter Vamplew, Benjamin J. Smith, Johan K\u00e4llstr\u00f6m, Gabriel de Oliveira Ramos, Roxana Radulescu, Diederik M. Roijers, Conor F. Hayes, Fredrik Heintz, Patrick Mannion, Pieter J. K. Libin, Richard Dazeley, and Cameron Foale. 2022. Scalar reward is not enough: a response to Silver, Singh, Precup and Sutton (2021). AAMAS 36, 2 (2022), 41.","journal-title":"AAMAS"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527448"},{"key":"e_1_3_2_1_50_1","volume-title":"Dullerud","author":"Wang Yu","year":"2020","unstructured":"Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud. 2020. Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning. In CDC. IEEE, 1392\u20131397."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2023.119401"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-023-09633-6"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"He Zhu Zikang Xiong Stephen Magill and Suresh Jagannathan. 2019. An inductive synthesis framework for verifiable reinforcement learning. In PLDI. ACM 686\u2013701.","DOI":"10.1145\/3314221.3314638"}],"event":{"name":"SAC '25: 40th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Catania International Airport Catania Italy","acronym":"SAC '25"},"container-title":["Proceedings of the 40th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707759","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3672608.3707759","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:32Z","timestamp":1750298252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":52,"alternative-id":["10.1145\/3672608.3707759","10.1145\/3672608"],"URL":"https:\/\/doi.org\/10.1145\/3672608.3707759","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]},"assertion":[{"value":"2025-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}