{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,20]],"date-time":"2025-12-20T02:21:30Z","timestamp":1766197290467,"version":"3.40.3"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308222"},{"type":"electronic","value":"9783031308239"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_1","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"3-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Mathias","family":"Lechner","sequence":"additional","affiliation":[]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: FOSSIL: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. In: Bogomolov, S., Jungers, R.M. (eds.) HSCC \u201921: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021. pp. 24:1\u201324:11. ACM (2021). https:\/\/doi.org\/10.1145\/3447928.3456646, https:\/\/doi.org\/10.1145\/3447928.3456646","DOI":"10.1145\/3447928.3456646"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Abate, A., Ahmed, D., Giacobbe, M., Peruffo, A.: Formal synthesis of lyapunov neural networks. IEEE Control. Syst. Lett. 5(3), 773\u2013778 (2021). https:\/\/doi.org\/10.1109\/LCSYS.2020.3005328, https:\/\/doi.org\/10.1109\/LCSYS.2020.3005328","DOI":"10.1109\/LCSYS.2020.3005328"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 3\u201326. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1, https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"1_CR4","unstructured":"Achiam, J., Held, D., Tamar, A., Abbeel, P.: Constrained policy optimization. In: International Conference on Machine Learning. pp. 22\u201331. PMLR (2017)"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL), 34:1\u201334:32 (2018). https:\/\/doi.org\/10.1145\/3158122, https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Aksaray, D., Jones, A., Kong, Z., Schwager, M., Belta, C.: Q-learning for robust satisfaction of signal temporal logic specifications. In: 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016. pp. 6565\u20136570. IEEE (2016). https:\/\/doi.org\/10.1109\/CDC.2016.7799279, https:\/\/doi.org\/10.1109\/CDC.2016.7799279","DOI":"10.1109\/CDC.2016.7799279"},{"key":"1_CR7","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. pp. 2669\u20132678. AAAI Press (2018), https:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI18\/paper\/view\/17211"},{"key":"1_CR8","unstructured":"Altman, E.: Constrained Markov decision processes, vol.\u00a07. CRC Press (1999)"},{"key":"1_CR9","unstructured":"Amodei, D., Olah, C., Steinhardt, J., Christiano, P.F., Schulman, J., Man\u00e9, D.: Concrete problems in AI safety. CoRR abs\/1606.06565 (2016), http:\/\/arxiv.org\/abs\/1606.06565"},{"key":"1_CR10","unstructured":"Anderson, G., Verma, A., Dillig, I., Chaudhuri, S.: Neurosymbolic reinforcement learning with formally verified exploration. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020), https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/448d5eda79895153938a8431919f4c9f-Abstract.html"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event \/ Montreal, Canada, 19-27 August 2021. pp. 2154\u20132160. ijcai.org (2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/297, https:\/\/doi.org\/10.24963\/ijcai.2021\/297","DOI":"10.24963\/ijcai.2021\/297"},{"key":"1_CR12","unstructured":"Brafman, R.I., Giacomo, G.D., Patrizi, F.: Ltlf\/ldlf non-markovian rewards. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. pp. 1771\u20131778. AAAI Press (2018), https:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI18\/paper\/view\/17342"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Camacho, A., Icarte, R.T., Klassen, T.Q., Valenzano, R.A., McIlraith, S.A.: LTL and beyond: Formal languages for reward function specification in reinforcement learning. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019. pp. 6065\u20136073. ijcai.org (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/840, https:\/\/doi.org\/10.24963\/ijcai.2019\/840","DOI":"10.24963\/ijcai.2019\/840"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Cauchi, N., Abate, A.: Stochy-automated verification and synthesis of stochastic processes. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. pp. 258\u2013259 (2019)","DOI":"10.1145\/3302504.3313349"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08044, pp. 511\u2013526. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Voronin, Y., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09636, pp. 260\u2013279. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15, https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Chang, Y., Gao, S.: Stabilizing neural control using self-learned almost lyapunov critics. In: IEEE International Conference on Robotics and Automation, ICRA 2021, Xi\u2019an, China, May 30 - June 5, 2021. pp. 1803\u20131809. IEEE (2021). https:\/\/doi.org\/10.1109\/ICRA48506.2021.9560886, https:\/\/doi.org\/10.1109\/ICRA48506.2021.9560886","DOI":"10.1109\/ICRA48506.2021.9560886"},{"key":"1_CR18","unstructured":"Chang, Y., Roohi, N., Gao, S.: Neural lyapunov control. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 3240\u20133249 (2019), https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/2647c1dba23bc0e0f9cdf75339e120d2-Abstract.html"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09779, pp. 3\u201322. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1, https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 327\u2013342. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837639, https:\/\/doi.org\/10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 55\u201378. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4, https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Z\u00e1rev\u00facky, J., Zikelic, D.: On lexicographic proof rules for probabilistic termination. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13047, pp. 619\u2013639. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33, https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33","DOI":"10.1007\/978-3-030-90870-6_33"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 145\u2013160. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009873, https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973, https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Crespo, L.G., Sun, J.: Stochastic optimal control via bellman\u2019s principle. Autom. 39(12), 2109\u20132114 (2003). https:\/\/doi.org\/10.1016\/S0005-1098(03)00238-3, https:\/\/doi.org\/10.1016\/S0005-1098(03)00238-3","DOI":"10.1016\/S0005-1098(03)00238-3"},{"key":"1_CR26","unstructured":"Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods. CoRR abs\/2202.11762 (2022), https:\/\/arxiv.org\/abs\/2202.11762"},{"key":"1_CR27","unstructured":"Garc\u00eda, J., Fern\u00e1ndez, F.: A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res. 16, 1437\u20131480 (2015), http:\/\/dl.acm.org\/citation.cfm?id=2886795"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Geibel, P.: Reinforcement learning for mdps with constraints. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04212, pp. 646\u2013653. Springer (2006). https:\/\/doi.org\/10.1007\/11871842_63, https:\/\/doi.org\/10.1007\/11871842_63","DOI":"10.1007\/11871842_63"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Giacobbe, M., Hasanbeig, M., Kroening, D., Wijk, H.: Shielding atari games with bounded prescience. In: Dignum, F., Lomuscio, A., Endriss, U., Now\u00e9, A. (eds.) AAMAS \u201921: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021. pp. 1507\u20131509. ACM (2021). https:\/\/doi.org\/10.5555\/3463952.3464141, https:\/\/www.ifaamas.org\/Proceedings\/aamas2021\/pdfs\/p1507.pdf","DOI":"10.5555\/3463952.3464141"},{"key":"1_CR30","unstructured":"Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T.A., Kohli, P.: On the effectiveness of interval bound propagation for training verifiably robust models. CoRR abs\/1810.12715 (2018), http:\/\/arxiv.org\/abs\/1810.12715"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Omega-regular objectives in model-free reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11427, pp. 395\u2013412. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_27, https:\/\/doi.org\/10.1007\/978-3-030-17462-0_27","DOI":"10.1007\/978-3-030-17462-0_27"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Hasanbeig, M., Kantaros, Y., Abate, A., Kroening, D., Pappas, G.J., Lee, I.: Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees. In: 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019. pp. 5338\u20135343. IEEE (2019). https:\/\/doi.org\/10.1109\/CDC40024.2019.9028919, https:\/\/doi.org\/10.1109\/CDC40024.2019.9028919","DOI":"10.1109\/CDC40024.2019.9028919"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Henrion, D., Garulli, A.: Positive polynomials in control, vol.\u00a0312. Springer Science & Business Media (2005)","DOI":"10.1007\/b96977"},{"key":"1_CR34","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), http:\/\/proceedings.mlr.press\/v80\/icarte18a.html"},{"key":"1_CR35","unstructured":"Inala, J.P., Bastani, O., Tavares, Z., Solar-Lezama, A.: Synthesizing programmatic policies that inductively generalize. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net (2020), https:\/\/openreview.net\/forum?id=S1l8oANFDH"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Jansen, N., K\u00f6nighofer, B., Junges, S., Serban, A., Bloem, R.: Safe reinforcement learning using probabilistic shields (invited paper). In: Konnov, I., Kov\u00e1cs, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference). LIPIcs, vol.\u00a0171, pp. 3:1\u20133:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.3, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.3","DOI":"10.4230\/LIPIcs.CONCUR.2020.3"},{"key":"1_CR37","unstructured":"Jarvis-Wloszek, Z., Feeley, R., Tan, W., Sun, K., Packard, A.: Some controls applications of sum of squares programming. In: 42nd IEEE international conference on decision and control (IEEE Cat. No. 03CH37475). vol.\u00a05, pp. 4676\u20134681. IEEE (2003)"},{"key":"1_CR38","unstructured":"Jin, W., Wang, Z., Yang, Z., Mou, S.: Neural certificates for safe control policies. CoRR abs\/2006.08465 (2020), https:\/\/arxiv.org\/abs\/2006.08465"},{"key":"1_CR39","unstructured":"Jothimurugan, K., Alur, R., Bastani, O.: A composable specification language for reinforcement learning tasks. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 13021\u201313030 (2019), https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/f5aa4bd09c07d8b2f65bad6c7cd3358f-Abstract.html"},{"key":"1_CR40","unstructured":"Jothimurugan, K., Bansal, S., Bastani, O., Alur, R.: Compositional reinforcement learning from logical specifications. In: Ranzato, M., Beygelzimer, A., Dauphin, Y.N., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual. pp. 10026\u201310039 (2021), https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/531db99cb00833bcd414459069dc7387-Abstract.html"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Kushner, H.J.: A partial history of the early development of continuous-time nonlinear stochastic systems theory. Autom. 50(2), 303\u2013334 (2014). https:\/\/doi.org\/10.1016\/j.automatica.2013.10.013, https:\/\/doi.org\/10.1016\/j.automatica.2013.10.013","DOI":"10.1016\/j.automatica.2013.10.013"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Lavaei, A., Khaled, M., Soudjani, S., Zamani, M.: AMYTISS: parallelized automated controller synthesis for large-scale stochastic systems. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 461\u2013474. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_24, https:\/\/doi.org\/10.1007\/978-3-030-53291-8_24","DOI":"10.1007\/978-3-030-53291-8_24"},{"key":"1_CR43","unstructured":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T.A.: Infinite time horizon safety of bayesian neural networks. In: Ranzato, M., Beygelzimer, A., Dauphin, Y.N., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual. pp. 10171\u201310185 (2021), https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/544defa9fddff50c53b71c43e0da72be-Abstract.html"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022. pp. 7326\u20137336. AAAI Press (2022), https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/20695","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"1_CR45","doi-asserted-by":"publisher","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 2017, Vancouver, BC, Canada, September 24-28, 2017. pp. 3834\u20133839. IEEE (2017). https:\/\/doi.org\/10.1109\/IROS.2017.8206234, https:\/\/doi.org\/10.1109\/IROS.2017.8206234","DOI":"10.1109\/IROS.2017.8206234"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Lyapunov, A.M.: The general problem of the stability of motion. International journal of control 55(3), 531\u2013534 (1992)","DOI":"10.1080\/00207179208934253"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121, https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"1_CR48","unstructured":"Murphy, K.P.: Machine learning - a probabilistic perspective. Adaptive computation and machine learning series, MIT Press (2012)"},{"key":"1_CR49","unstructured":"Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. California Institute of Technology (2000)"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control. 52(8), 1415\u20131428 (2007). https:\/\/doi.org\/10.1109\/TAC.2007.902736, https:\/\/doi.org\/10.1109\/TAC.2007.902736","DOI":"10.1109\/TAC.2007.902736"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887, https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"1_CR52","unstructured":"Qin, Z., Zhang, K., Chen, Y., Chen, J., Fan, C.: Learning safe multi-agent control with decentralized neural barrier certificates. In: 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net (2021), https:\/\/openreview.net\/forum?id=P6_q1BRxY8Q"},{"key":"1_CR53","unstructured":"Richards, S.M., Berkenkamp, F., Krause, A.: The lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems. In: 2nd Annual Conference on Robot Learning, CoRL 2018, Z\u00fcrich, Switzerland, 29-31 October 2018, Proceedings. Proceedings of Machine Learning Research, vol.\u00a087, pp. 466\u2013476. PMLR (2018), http:\/\/proceedings.mlr.press\/v87\/richards18a.html"},{"key":"1_CR54","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347 (2017)"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006. pp. 404\u2013415. ACM (2006). https:\/\/doi.org\/10.1145\/1168857.1168907, https:\/\/doi.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST $${}^{ \\text{2}}$$ : Formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 272\u2013286. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_23, https:\/\/doi.org\/10.1007\/978-3-662-46681-0_23","DOI":"10.1007\/978-3-662-46681-0_23"},{"key":"1_CR57","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: Bengio, Y., LeCun, Y. (eds.) 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings (2014), http:\/\/arxiv.org\/abs\/1312.6199"},{"key":"1_CR58","unstructured":"Taylor, A.J., Singletary, A., Yue, Y., Ames, A.D.: Learning for safety-critical control with control barrier functions. In: Bayen, A.M., Jadbabaie, A., Pappas, G.J., Parrilo, P.A., Recht, B., Tomlin, C.J., Zeilinger, M.N. (eds.) Proceedings of the 2nd Annual Conference on Learning for Dynamics and Control, L4DC 2020, Online Event, Berkeley, CA, USA, 11-12 June 2020. Proceedings of Machine Learning Research, vol.\u00a0120, pp. 708\u2013717. PMLR (2020), http:\/\/proceedings.mlr.press\/v120\/taylor20a.html"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Uchibe, E., Doya, K.: Constrained reinforcement learning from intrinsic and extrinsic rewards. In: 2007 IEEE 6th International Conference on Development and Learning. pp. 163\u2013168. IEEE (2007)","DOI":"10.1109\/DEVLRN.2007.4354030"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Vaidya, U.: Stochastic stability analysis of discrete-time system using lyapunov measure. In: American Control Conference, ACC 2015, Chicago, IL, USA, July 1-3, 2015. pp. 4646\u20134651. IEEE (2015). https:\/\/doi.org\/10.1109\/ACC.2015.7172061, https:\/\/doi.org\/10.1109\/ACC.2015.7172061","DOI":"10.1109\/ACC.2015.7172061"},{"key":"1_CR61","unstructured":"Verma, A., Le, H.M., Yue, Y., Chaudhuri, S.: Imitation-projected programmatic reinforcement learning. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 15726\u201315737 (2019), https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/5a44a53b7d26bb1e54c05222f186dcfb-Abstract.html"},{"key":"1_CR62","unstructured":"Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable 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. 5052\u20135061. PMLR (2018), http:\/\/proceedings.mlr.press\/v80\/verma18a.html"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Vinod, A.P., Gleason, J.D., Oishi, M.M.K.: Sreachtools: a MATLAB stochastic reachability toolbox. 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. 33\u201338. ACM (2019). https:\/\/doi.org\/10.1145\/3302504.3311809, https:\/\/doi.org\/10.1145\/3302504.3311809","DOI":"10.1145\/3302504.3311809"},{"key":"1_CR64","doi-asserted-by":"publisher","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 1171\u20131186. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454102, https:\/\/doi.org\/10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"1_CR65","doi-asserted-by":"publisher","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Costanalysis of nondeterministic probabilistic programs. In: McKinley, K.S.,Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 204\u2013220. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314581, https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"},{"key":"1_CR66","unstructured":"Williams, D.: Probability with Martingales. Cambridge mathematical textbooks, Cambridge University Press (1991)"},{"key":"1_CR67","doi-asserted-by":"publisher","unstructured":"Zhu, H., Xiong, Z., Magill, S., Jagannathan, S.: An inductive synthesis framework for verifiable reinforcement learning. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 686\u2013701. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314638, https:\/\/doi.org\/10.1145\/3314221.3314638","DOI":"10.1145\/3314221.3314638"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Zikelic, D., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. To appear at the Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23) (2023)","DOI":"10.1609\/aaai.v37i10.26407"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T10:02:08Z","timestamp":1691143328000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}