{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:23:02Z","timestamp":1762816982034,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":25,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819542123","type":"print"},{"value":"9789819542130","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"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":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_19","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:17Z","timestamp":1762816697000},"page":"348-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling of\u00a0Reinforcement Learning Systems with\u00a0SMT"],"prefix":"10.1007","author":[{"given":"Tianyi","family":"Ding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxin","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"issue":"7587","key":"19_CR1","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., et al.: Mastering the game of go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016)","journal-title":"Nature"},{"key":"19_CR2","unstructured":"Silver, D., et al.: Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm. arXiv preprint arXiv:1712.01815 (2017)"},{"key":"19_CR3","unstructured":"Bostrom, A., et al.: AlphaStar: Grandmaster Level in StarCraft II using Multi-Agent Reinforcement Learning. arXiv preprint arXiv:1911.08265 (2019)"},{"key":"19_CR4","unstructured":"Ng, A.Y., Schojet, R., DeLeon, M., Thrun, S.: Playing catch with a robot hand. In: Proceedings of the 2009 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 1532\u20131537 (2009)"},{"key":"19_CR5","unstructured":"Raffin, E., et al.: Dactyl: Mastering the Dexterous Manipulation of Real Objects. arXiv preprint arXiv:2011.04962 (2020)"},{"issue":"6","key":"19_CR6","doi-asserted-by":"publisher","first-page":"4909","DOI":"10.1109\/TITS.2021.3054625","volume":"23","author":"BR Kiran","year":"2021","unstructured":"Kiran, B.R., et al.: Deep reinforcement learning for autonomous driving: a survey. IEEE Trans. Intell. Transp. Syst. 23(6), 4909\u20134926 (2021)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Sallab, A.E., Abdou, M., Perot, E., Yogamani, S.: Deep Reinforcement Learning Framework for Autonomous Driving. arXiv preprint arXiv:1704.02532 (2017)","DOI":"10.2352\/ISSN.2470-1173.2017.19.AVM-023"},{"key":"19_CR8","unstructured":"Krause, J., Lu, Y., Sun, W., Sun, M., Huang, X.: DeepMind\u2019s AI Predicts Hospital patient Deaths with 70"},{"issue":"7827","key":"19_CR9","first-page":"546","volume":"586","author":"J Jumper","year":"2020","unstructured":"Jumper, J., et al.: AlphaFold: a solution to a 50-year-old grand challenge in biology. Nature 586(7827), 546\u2013551 (2020)","journal-title":"Nature"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Li, J., Monroe, W., Ritter, A., Galley, M., Gao, J., Jurafsky, D.: Deep reinforcement learning for dialogue generation. arXiv preprint arXiv:1606.01541 (2016)","DOI":"10.18653\/v1\/D16-1127"},{"issue":"7","key":"19_CR11","first-page":"2469","volume":"31","author":"Y Keneshloo","year":"2019","unstructured":"Keneshloo, Y., Shi, T., Ramakrishnan, N., Reddy, C.K.: Deep reinforcement learning for sequence-to-sequence models. IEEE Trans. Neural Netw. Learn. Syst. 31(7), 2469\u20132489 (2019)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"issue":"2","key":"19_CR12","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1007\/s10462-022-10205-5","volume":"56","author":"V Uc-Cetina","year":"2023","unstructured":"Uc-Cetina, V., Navarro-Guerrero, N., Martin-Gonzalez, A., Weber, C., Wermter, S.: Survey on reinforcement learning for language processing. Artif. Intell. Rev. 56(2), 1543\u20131575 (2023)","journal-title":"Artif. Intell. Rev."},{"key":"19_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2020.106706","volume":"213","author":"L Huang","year":"2021","unstructured":"Huang, L., Fu, M., Li, F., Qu, H., Liu, Y., Chen, W.: A deep reinforcement learning based long-term recommender system. Knowl.-Based Syst. 213, 106706 (2021)","journal-title":"Knowl.-Based Syst."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Lei, Y., Pei, H., Yan, H., Li, W.: Reinforcement learning based recommendation with graph convolutional Q-Network. In: Proceedings of the 43rd International ACM SIGIR Conference on Research and Development in Information Retrieval, pp. 1757\u20131760 (2020)","DOI":"10.1145\/3397271.3401237"},{"issue":"3","key":"19_CR15","doi-asserted-by":"publisher","first-page":"274","DOI":"10.3991\/ijet.v16i03.18851","volume":"16","author":"U Javed","year":"2021","unstructured":"Javed, U., Shaukat, K., Hameed, I.A., Iqbal, F., Alam, T.M., Luo, S.: A review of content-based and context-based recommendation systems. Int. J. Emerg. Technol. Learn. (iJET) 16(3), 274\u2013306 (2021)","journal-title":"Int. J. Emerg. Technol. Learn. (iJET)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1609\/aaai.v32i1.12107"},{"key":"19_CR17","unstructured":"Chen, W.: Formal Modeling and Automatic Generation of Test Cases for the Autonomous Vehicle. Ph.D. thesis, Universit\u00e9 Paris-Saclay (2020)"},{"key":"19_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2022.102701","volume":"131","author":"Y Lu","year":"2022","unstructured":"Lu, Y., Sun, W., Sun, M.: Towards mutation testing of reinforcement learning systems. J. Syst. Architect. 131, 102701 (2022)","journal-title":"J. Syst. Architect."},{"key":"19_CR19","unstructured":"Bacci, E.: Formal Verification of Deep Reinforcement Learning Agents. Ph.D. thesis, University of Birmingham (2022)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Varshosaz, M., Ghaffari, M., Johnsen, E.B., W\u0105sowski, A.: Formal specification and testing for reinforcement learning. Proc. ACM Program. Lang. 7(ICFP), 125\u2013158 (2023)","DOI":"10.1145\/3607835"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Gross, D., Spieker, H.: Probabilistic model checking of stochastic reinforcement learning policies. arXiv preprint arXiv:2403.18725 (2024)","DOI":"10.5220\/0012357700003636"},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"Zhang, X., Sun, M.: SMT-based modeling and verification of cloud applications. In: Xia, Y., Zhang, L.J. (eds.) Services \u2013 SERVICES 2019. SERVICES 2019. LNCS, vol. 11517, pp. 1\u201315. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23381-5_1","DOI":"10.1007\/978-3-030-23381-5_1"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Wei, Z., Zhang, X., Sun, M.: Using Z3 for Formal Modeling and Verification of FNN Global Robustness. arXiv preprint arXiv:2304.10558 (2023)","DOI":"10.18293\/SEKE2023-110"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. LNCS, vol. 12652, pp. 203\u2013222. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"19_CR25","unstructured":"Maucher, J.: Example Q-Learning (2022). https:\/\/hannibunny.github.io\/mlbook\/rl\/QLearnFrozenLake.html. Accessed 16 Sep 2021"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:19Z","timestamp":1762816699000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}