{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:25:14Z","timestamp":1760142314988,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We propose a deductive synthesis framework for constructing reinforcement learning (RL) agents that provably satisfy temporal reach-avoid specifications over infinite horizons. Our approach decomposes these temporal specifications into a sequence of finite-horizon subtasks, for which we synthesize individual RL policies. Using formal verification techniques, we ensure that the composition of a finite number of subtask policies guarantees satisfaction of the overall specification over infinite horizons. Experimental results on a suite of benchmarks show that our synthesized agents outperform standard RL methods in both task performance and compliance with safety and temporal requirements.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_4","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:31:51Z","timestamp":1753155111000},"page":"79-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deductive Synthesis of\u00a0Reinforcement Learning Agents for\u00a0Infinite Horizon Tasks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4317-9758","authenticated-orcid":false,"given":"Yuning","family":"Wang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9606-150X","authenticated-orcid":false,"given":"He","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011, pp. 273\u2013278. ACM (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, A., Deshmukh, J.V.: Structured reward shaping using signal temporal logic specifications. In: 2019 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3481\u20133486 (2019)","DOI":"10.1109\/IROS40897.2019.8968254"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1146\/annurev-control-053018-023717","volume":"2","author":"C Belta","year":"2019","unstructured":"Belta, C., Sadraddini, S.: Formal methods for control synthesis: an optimization perspective. Annu. Rev. Control. Robotics Auton. Syst. 2, 115\u2013140 (2019)","journal-title":"Annu. Rev. Control. Robotics Auton. Syst."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Bozkurt, A.K., Wang, Y., Zavlanos, M.M., Pajic, M.: Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In: 2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, France, May 31 - August 31, 2020, pp. 10349\u201310355. IEEE (2020)","DOI":"10.1109\/ICRA40945.2020.9196796"},{"issue":"4","key":"4_CR5","doi-asserted-by":"publisher","first-page":"7973","DOI":"10.1109\/LRA.2021.3101544","volume":"6","author":"M Cai","year":"2021","unstructured":"Cai, M., Hasanbeig, M., Xiao, S., Abate, A., Kan, Z.: Modular deep reinforcement learning for continuous motion planning with temporal logic. IEEE Robot. Autom. Lett. 6(4), 7973\u20137980 (2021)","journal-title":"IEEE Robot. Autom. Lett."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Camacho, A., Icarte, R.T., Klassen, T.Q., Valenzano, R., McIlraith, S.A.: LTL and beyond: Formal languages for reward function specification in reinforcement learning. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19), pp. 6065\u20136073. International Joint Conferences on Artificial Intelligence Organization (2019)","DOI":"10.24963\/ijcai.2019\/840"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-41528-4_6","volume-title":"Computer Aided Verification","author":"C-H Cheng","year":"2016","unstructured":"Cheng, C.-H., Hamza, Y., Ruess, H.: Structural synthesis for GXW specifications. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 95\u2013117. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_6"},{"issue":"11","key":"4_CR9","doi-asserted-by":"publisher","first-page":"1883","DOI":"10.1109\/TAC.2002.804474","volume":"47","author":"J Daafouz","year":"2002","unstructured":"Daafouz, J., Riedinger, P., Iung, C.: Stability analysis and control synthesis for switched systems: a switched Lyapunov function approach. IEEE Trans. Autom. Control 47(11), 1883\u20131887 (2002)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR10","unstructured":"Delgrange, F., Avni, G., Lukina, A., Schilling, C., Now\u00e9, A., P\u00e9rez, G.A.: Synthesis of hierarchical controllers based on deep reinforcement learning policies. CoRR abs\/2402.13785 (2024)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Ozay, N., Prabhakar, P. (eds.) Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pp. 157\u2013168. ACM (2019)","DOI":"10.1145\/3302504.3311807"},{"issue":"2","key":"4_CR12","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Autom. 45(2), 343\u2013352 (2009)","journal-title":"Autom."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-030-59152-6_30","volume-title":"Automated Technology for Verification and Analysis","author":"J Fan","year":"2020","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 537\u2013542. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30"},{"key":"4_CR14","unstructured":"Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. CoRR abs\/1010.4672 (2010)"},{"issue":"5","key":"4_CR15","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A Girard","year":"2007","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782\u2013798 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR16","unstructured":"Haarnoja, T., Zhou, A., Abbeel, P., Levine, S.: Soft actor-critic: off-policy maximum entropy deep reinforcement learning with a stochastic actor (2018). https:\/\/arxiv.org\/abs\/1801.01290"},{"key":"4_CR17","unstructured":"Hasanbeig, M., Kroening, D., Abate, A.: Towards verifiable and safe model-free reinforcement learning. In: CEUR Workshop Proceedings, vol.\u00a02509 (2020)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-57628-8_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Hasanbeig","year":"2020","unstructured":"Hasanbeig, M., Kroening, D., Abate, A.: Deep reinforcement learning with temporal logics. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 1\u201322. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_1"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.: Lazy abstraction-based control for safety specifications. In: 57th IEEE Conference on Decision and Control, CDC 2018, Miami, FL, USA, December 17-19, 2018, pp. 4902\u20134907. IEEE (2018)","DOI":"10.1109\/CDC.2018.8619659"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Icarte, R.T., Klassen, T.Q., Valenzano, R., McIlraith, S.A.: Reward machines: exploiting reward function structure in reinforcement learning. J. Artif. Intell. Res. 73, 173\u2013208 (2022)","DOI":"10.1613\/jair.1.12440"},{"key":"4_CR21","unstructured":"Icarte, R.T., Klassen, T.Q., Valenzano, R.A., McIlraith, S.A.: Using reward machines for high-level task specification and decomposition in reinforcement learning. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, July 10-15, 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 2112\u20132121. PMLR (2018)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Ozay, N., Prabhakar, P. (eds.) Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pp. 169\u2013178. ACM (2019)","DOI":"10.1145\/3302504.3311806"},{"issue":"3","key":"4_CR23","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1109\/87.491203","volume":"4","author":"M Jankovic","year":"1996","unstructured":"Jankovic, M., Fontaine, D., Kokotovic, P.V.: Tora example: cascade- and passivity-based control designs. IEEE Trans. Control Syst. Technol. 4(3), 292\u2013297 (1996)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-031-13185-1_10","volume-title":"Computer Aided Verification","author":"P Jin","year":"2022","unstructured":"Jin, P., Tian, J., Zhi, D., Wen, X., Zhang, M.: TRAINIFY: A CEGAR-driven training and verification framework for safe deep reinforcement learning. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 193\u2013218. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_10"},{"key":"4_CR25","unstructured":"Johnson, T.T., et al.: ARCH-COMP21 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021. EPiC Series in Computing, vol.\u00a080, pp. 90\u2013119. EasyChair (2021)"},{"key":"4_CR26","volume-title":"A Composable Specification Language for Reinforcement Learning Tasks","author":"K Jothimurugan","year":"2019","unstructured":"Jothimurugan, K., Alur, R., Bastani, O.: A Composable Specification Language for Reinforcement Learning Tasks. Curran Associates Inc., Red Hook, NY, USA (2019)"},{"key":"4_CR27","unstructured":"Jothimurugan, K., Bansal, S., Bastani, O., Alur, R.: Compositional reinforcement learning from logical specifications. In: Proceedings of the 35th International Conference on Neural Information Processing Systems. NIPS 2021, Curran Associates Inc., Red Hook, NY, USA (2024)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-642-14295-6_49","volume-title":"Computer Aided Verification","author":"M Mazo","year":"2010","unstructured":"Mazo, M., Davitian, A., Tabuada, P.: PESSOA: a tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566\u2013569. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_49"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1016\/j.automatica.2017.04.060","volume":"83","author":"ES Kim","year":"2017","unstructured":"Kim, E.S., Arcak, M., Seshia, S.A.: Symbolic control design for monotone systems with directed specifications. Autom. 83, 10\u201319 (2017)","journal-title":"Autom."},{"issue":"6","key":"4_CR30","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Robot."},{"issue":"5","key":"4_CR31","doi-asserted-by":"publisher","first-page":"3791","DOI":"10.1109\/TRO.2023.3291463","volume":"39","author":"V Kurtz","year":"2023","unstructured":"Kurtz, V., Lin, H.: Temporal logic motion planning with convex optimization via graphs of convex sets. IEEE Trans. Robot. 39(5), 3791\u20133804 (2023)","journal-title":"IEEE Trans. Robot."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Li, X., Vasile, C.I., Belta, C.: Reinforcement learning with temporal logic rewards. In: 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3834\u20133839 (2017)","DOI":"10.1109\/IROS.2017.8206234"},{"key":"4_CR33","unstructured":"Mania, H., Guy, A., Recht, B.: Simple random search provides a competitive approach to reinforcement learning (2018). https:\/\/arxiv.org\/abs\/1803.07055"},{"issue":"11","key":"4_CR34","doi-asserted-by":"publisher","first-page":"4676","DOI":"10.1109\/TAC.2019.2902643","volume":"64","author":"P Meyer","year":"2019","unstructured":"Meyer, P., Dimarogonas, D.V.: Hierarchical decomposition of LTL synthesis problem for nonlinear control systems. IEEE Trans. Autom. Control 64(11), 4676\u20134683 (2019)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR35","volume-title":"Efficient Memory-Based Learning for Robot Control","author":"AW Moore","year":"1990","unstructured":"Moore, A.W.: Efficient Memory-Based Learning for Robot Control. University of Cambridge, Tech. rep. (1990)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Mouelhi, S., Girard, A., G\u00f6\u00dfler, G.: CoSyMA: a tool for controller synthesis using multi-scale abstractions. In: Belta, C., Ivancic, F. (eds.) Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, April 8-11, 2013, Philadelphia, PA, USA, pp. 83\u201388. ACM (2013)","DOI":"10.1145\/2461328.2461343"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_24"},{"issue":"10","key":"4_CR38","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G Pola","year":"2008","unstructured":"Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Autom. 44(10), 2508\u20132516 (2008)","journal-title":"Autom."},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"key":"4_CR40","unstructured":"Qiu, W., Mao, W., Zhu, H.: Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. In: Thirty-seventh Conference on Neural Information Processing Systems (2023)"},{"issue":"4","key":"4_CR41","doi-asserted-by":"publisher","first-page":"1781","DOI":"10.1109\/TAC.2016.2593947","volume":"62","author":"G Reissig","year":"2017","unstructured":"Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781\u20131796 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Ren, W., Dimarogonas, D.V.: Logarithmic quantization based symbolic abstractions for nonlinear control systems. In: 17th European Control Conference, ECC 2019, Naples, Italy, June 25-28, 2019, pp. 1312\u20131317. IEEE (2019)","DOI":"10.23919\/ECC.2019.8795730"},{"issue":"11","key":"4_CR43","doi-asserted-by":"publisher","first-page":"7630","DOI":"10.1109\/TAC.2024.3394313","volume":"69","author":"W Ren","year":"2024","unstructured":"Ren, W., Jungers, R.M., Dimarogonas, D.V.: Zonotope-based symbolic controller synthesis for linear temporal logic specifications. IEEE Trans. Autom. Control 69(11), 7630\u20137645 (2024)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Rungger, M., Zamani, M.: SCOTS: A tool for the synthesis of symbolic controllers. In: Abate, A., Fainekos, G. (eds.) Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016, pp. 99\u2013104. ACM (2016)","DOI":"10.1145\/2883817.2883834"},{"key":"4_CR45","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms (2017). https:\/\/arxiv.org\/abs\/1707.06347"},{"key":"4_CR46","unstructured":"Shah, A., Voloshin, C., Yang, C., Verma, A., Chaudhuri, S., Seshia, S.A.: LTL-constrained policy optimization with cycle experience replay (2024). https:\/\/arxiv.org\/abs\/2404.11578"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Shao, D., Kwiatkowska, M.: Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees. In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China pp. 4180\u20134189. ijcai.org (2023)","DOI":"10.24963\/ijcai.2023\/465"},{"key":"4_CR48","unstructured":"Srinivasan, K., Eysenbach, B., Ha, S., Tan, J., Finn, C.: Learning to be safe: deep RL with a safety critic (2020). https:\/\/arxiv.org\/abs\/2010.14603"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Ozay, N., Prabhakar, P. (eds.) Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019 pp. 147\u2013156. ACM (2019)","DOI":"10.1145\/3302504.3311802"},{"issue":"8","key":"4_CR50","doi-asserted-by":"publisher","first-page":"1038","DOI":"10.1177\/0278364910369189","volume":"29","author":"R Tedrake","year":"2010","unstructured":"Tedrake, R., Manchester, I.R., Tobenkin, M.M., Roberts, J.W.: LQR-trees: feedback motion planning via sums-of-squares verification. Int. J. Robot. Res. 29(8), 1038\u20131052 (2010)","journal-title":"Int. J. Robot. Res."},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"4_CR52","doi-asserted-by":"crossref","unstructured":"Tumova, J., Yordanov, B., Belta, C., Cerna, I., Barnat, J.: A symbolic approach to controlling piecewise affine systems. In: Proceedings of the 49th IEEE Conference on Decision and Control, CDC 2010, December 15-17, 2010, Atlanta, Georgia, USA, pp. 4230\u20134235. IEEE (2010)","DOI":"10.1109\/CDC.2010.5717316"},{"key":"4_CR53","unstructured":"Vaezipoor, P., Li, A.C., Icarte, R.T., McIlraith, S.A.: Ltl2action: Generalizing LTL instructions for multi-task RL. In: Proceedings of the 38th International Conference on Machine Learning (ICML), vol.\u00a0139, pp. 10497\u201310508. Proceedings of Machine Learning Research (2021)"},{"key":"4_CR54","unstructured":"Voloshin, C., Verma, A., Yue, Y.: Eventual discounting temporal logic counterfactual experience replay. In: Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., Scarlett, J. (eds.) International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Proceedings of Machine Learning Research, vol.\u00a0202, pp. 35137\u201335150. PMLR (2023)"},{"key":"4_CR55","unstructured":"Wang, C., Li, Y., Smith, S.L., Liu, J.: Continuous motion planning with temporal logic specifications using deep neural networks (2020). https:\/\/arxiv.org\/abs\/2004.02610"},{"key":"4_CR56","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-031-30820-8_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Wang","year":"2023","unstructured":"Wang, Y., Zhu, H.: Verification-guided programmatic controller synthesis. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 229\u2013250. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_16"},{"key":"4_CR57","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-031-65633-0_11","volume-title":"Computer Aided Verification","author":"Y Wang","year":"2024","unstructured":"Wang, Y., Zhu, H.: Safe exploration in reinforcement learning by reachability analysis over learned models. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 232\u2013255. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_11"},{"key":"4_CR58","unstructured":"Wang, Y., Zhu, H.: Deductive synthesis of reinforcement learning agents for $$\\omega $$-regular properties (extended version) (2025). https:\/\/github.com\/RU-Automated-Reasoning-Group\/VEL-inf\/blob\/main\/VEL-inf_extended.pdf"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: Tulip: a software toolbox for receding horizon temporal logic planning. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pp. 313\u2013314. ACM (2011)","DOI":"10.1145\/1967701.1967747"},{"key":"4_CR60","unstructured":"Yang, L., Dai, H., Shi, Z., Hsieh, C.J., Tedrake, R., Zhang, H.: Lyapunov-stable neural control for state and output feedback: a novel formulation. In: Proceedings of the 41st International Conference on Machine Learning. ICML2024, JMLR.org (2024)"},{"key":"4_CR61","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Verma, A., Chatterjee, K., Henzinger, T.A.: Compositional policy learning in stochastic control systems with formal guarantees. In: Thirty-seventh Conference on Neural Information Processing Systems (2023)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:55:18Z","timestamp":1760086518000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}