{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T13:02:08Z","timestamp":1770814928607,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T00:00:00Z","timestamp":1634601600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T00:00:00Z","timestamp":1634601600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"National Science Foundation Graduate Research Fellowship","award":["DGE-1656518"],"award-info":[{"award-number":["DGE-1656518"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mach Learn"],"published-print":{"date-parts":[[2023,8]]},"DOI":"10.1007\/s10994-021-06065-9","type":"journal-article","created":{"date-parts":[[2021,10,19]],"date-time":"2021-10-19T22:34:05Z","timestamp":1634682845000},"page":"2903-2931","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Generating probabilistic safety guarantees for neural network controllers"],"prefix":"10.1007","volume":"112","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8376-5145","authenticated-orcid":false,"given":"Sydney M.","family":"Katz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6247-1874","authenticated-orcid":false,"given":"Kyle D.","family":"Julian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8914-6852","authenticated-orcid":false,"given":"Christopher A.","family":"Strong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7238-9663","authenticated-orcid":false,"given":"Mykel J.","family":"Kochenderfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,19]]},"reference":[{"key":"6065_CR1","unstructured":"Akintunde, M., Lomuscio, A., Maganti, L., & Pirovano, E. (2018). Reachability analysis for neural agent-environment systems. In International conference on principles of knowledge representation and reasoning, pp 184\u2013193."},{"key":"6065_CR2","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., & Lomuscio, A. (2020). Formal verification of neural agents in non-deterministic environments. In AAMAS, pp 25\u201333.","DOI":"10.1007\/s10458-021-09529-3"},{"key":"6065_CR3","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., & Katoen, J. P. (2008). Principles of model checking. MIT Press."},{"key":"6065_CR4","unstructured":"Bastani, O., Pu, Y., & Solar-Lezama, A. (2018). Verifiable reinforcement learning via policy extraction. arXiv preprint arXiv:180508328."},{"issue":"8","key":"6065_CR5","doi-asserted-by":"publisher","first-page":"716","DOI":"10.1073\/pnas.38.8.716","volume":"38","author":"R Bellman","year":"1952","unstructured":"Bellman, R. (1952). On the theory of dynamic programming. Proceedings of the National Academy of Sciences of the United States of America, 38(8), 716.","journal-title":"Proceedings of the National Academy of Sciences of the United States of America"},{"key":"6065_CR6","unstructured":"Bouton, M. (2020). Safe and scalable planning under uncertainty for autonomous driving. Ph.D. thesis, Stanford University, https:\/\/purl.stanford.edu\/dy440kv7606."},{"key":"6065_CR7","doi-asserted-by":"crossref","unstructured":"Bouton, M., Tumova, J., & Kochenderfer, M.J. (2020). Point-based methods for model checking in partially observable Markov decision processes. In AAAI conference on artificial intelligence (AAAI), https:\/\/aaai.org\/Papers\/AAAI\/2020GB\/AAAI-BoutonM.9314.pdf.","DOI":"10.1609\/aaai.v34i06.6563"},{"key":"6065_CR8","doi-asserted-by":"crossref","unstructured":"Carr, S., Jansen, N., & Topcu, U. (2020). Verifiable rnn-based policies for pomdps under temporal logic constraints. arXiv preprint arXiv:200205615.","DOI":"10.24963\/ijcai.2020\/570"},{"key":"6065_CR9","doi-asserted-by":"crossref","unstructured":"Clavi\u00e8re, A., Asselin, E., Garion, C., & Pagetti, C. (2020). Safety verification of neural network controlled systems. arXiv preprint arXiv:201105174.","DOI":"10.1109\/DSN-W52860.2021.00019"},{"key":"6065_CR10","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., & Sankaranarayanan, S. (2019). Reachability analysis for neural feedback systems using regressive polynomial rule inference. In ACM international conference on hybrid systems: Computation and control, pp 157\u2013168.","DOI":"10.1145\/3302504.3311807"},{"key":"6065_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019argenio, P.R., Jeannet, B., Jensen, H.E., & Larsen, K.G. (2001). Reachability analysis of probabilistic systems by successive refinements. In Joint international workshop on process algebra and probabilistic methods, performance modeling and verification, Springer, pp 39\u201356.","DOI":"10.1007\/3-540-44804-7_3"},{"issue":"5s","key":"6065_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., & Zhu, Q. (2019). ReachNN: Reachability analysis of neural-network controlled systems. ACM Transactions on Embedded Computing Systems (TECS), 18(5s), 1\u201322.","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"6065_CR13","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., & Lee, I. (2019). Verisig: Verifying safety properties of hybrid systems with neural network controllers. In ACM international conference on hybrid systems: Computation and Control, pp 169\u2013178.","DOI":"10.1145\/3302504.3311806"},{"key":"6065_CR14","doi-asserted-by":"publisher","unstructured":"Julian, K.D., & Kochenderfer, M.J. (2019a). Guaranteeing safety for neural network-based aircraft collision avoidance systems. In Digital avionics systems conference (dasc). https:\/\/doi.org\/10.1109\/DASC43569.2019.9081748. arXiv:org\/abs\/1912.07084.","DOI":"10.1109\/DASC43569.2019.9081748"},{"key":"6065_CR15","unstructured":"Julian, K.D., & Kochenderfer, M.J. (2019b). A reachability method for verifying dynamical systems with deep neural network controllers (1903.00520), arXiv:org\/abs\/1903.00520."},{"key":"6065_CR16","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7778091","author":"KD Julian","year":"2016","unstructured":"Julian, K. D., Lopez, J., Brush, J. S., Owen, M. P., & Kochenderfer, M. J. (2016). Policy compression for aircraft collision avoidance systems. Digital Avionics Systems Conference (DASC). https:\/\/doi.org\/10.1109\/DASC.2016.7778091.","journal-title":"Digital Avionics Systems Conference (DASC)"},{"issue":"3","key":"6065_CR17","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"KD Julian","year":"2019","unstructured":"Julian, K. D., Kochenderfer, M. J., & Owen, M. P. (2019a). Deep neural network compression for aircraft collision avoidance systems. AIAA Journal of Guidance, Control, and Dynamics, 42(3), 598\u2013608. https:\/\/doi.org\/10.2514\/1.G003724.","journal-title":"AIAA Journal of Guidance, Control, and Dynamics"},{"key":"6065_CR18","unstructured":"Julian, K.D, Sharma, S., Jeannin, J.B., & Kochenderfer, M.J. (2019b). Verifying aircraft collision avoidance neural networks through linear approximations of safe regions. In AIAA spring symposium, arXiv:org\/abs\/1903.00762."},{"key":"6065_CR19","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K.D., & Kochenderfer, M.J. (2017). Reluplex: An efficient SMT solver for verifying deep neural networks. In International conference on computer-aided verification. arXiv:org\/abs\/1702.01135.","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"6065_CR20","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D.A., Ibeling, D., Julian, K.D., Lazarus, C., Lim, R., Shah, P., Thakoor, S, Wu, H., & Zelji\u0107, A., Dill, D. L. (2019). The marabou framework for verification and analysis of deep neural networks. In International conference on computer aided verification. Springer, pp 443\u2013452.","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"6065_CR21","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/10187.001.0001","volume-title":"Decision making under uncertainty: Theory and application","author":"MJ Kochenderfer","year":"2015","unstructured":"Kochenderfer, M. J. (2015). Decision making under uncertainty: Theory and application. MIT Press."},{"key":"6065_CR22","unstructured":"Kochenderfer, M.J., & Chryssanthacopoulos, J. (2011). Robust airborne collision avoidance through dynamic programming. Massachusetts Institute of Technology, Lincoln Laboratory, Project Report ATC-371."},{"key":"6065_CR23","unstructured":"Kochenderfer, M. J., Holland, J. E., & Chryssanthacopoulos, J. P. (2012). Next-generation airborne collision avoidance system. Massachusetts Institute of Technology-Lincoln Laboratory Lexington United States: Tech. rep."},{"key":"6065_CR24","unstructured":"Koul, A., Greydanus, S., & Fern, A. (2018). Learning finite state representations of recurrent policy networks. arXiv preprint arXiv:181112530."},{"key":"6065_CR25","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Andersson, S., & Belta, C. (2011). Control of Markov decision processes from PCTL specifications. In American control conference, IEEE, pp 311\u2013316.","DOI":"10.1109\/ACC.2011.5990952"},{"issue":"3\u20134","key":"6065_CR26","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1561\/2400000035","volume":"4","author":"C Liu","year":"2021","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., & Kochenderfer, M. J. (2021). Algorithms for verifying deep neural networks. Foundations and Trends in Optimization, 4(3\u20134), 244\u2013404. https:\/\/doi.org\/10.1561\/2400000035.","journal-title":"Foundations and Trends in Optimization"},{"key":"6065_CR27","unstructured":"Lopez, D.M., Johnson, T., Tran, H.D., Bak, S., Chen, X., & Hobbs, K.L. (2021). Verification of neural network compression of ACAS Xu lookup tables with star set reachability. In AIAA Scitech Forum. p 0995."},{"issue":"7540","key":"6065_CR28","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., Kavukcuoglu, K., Silver, D., Rusu, A. A., Veness, J., Bellemare, M. G., Graves, A., Riedmiller, M., Fidjeland, A. K., Ostrovski, G., et al. (2015). Human-level control through deep reinforcement learning. Nature, 518(7540), 529\u2013533.","journal-title":"Nature"},{"issue":"2\u20133","key":"6065_CR29","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1017992615625","volume":"49","author":"R Munos","year":"2002","unstructured":"Munos, R., & Moore, A. (2002). Variable resolution discretization in optimal control. Machine Learning, 49(2\u20133), 291\u2013323.","journal-title":"Machine Learning"},{"key":"6065_CR30","unstructured":"Olson, W.A. (2015). Airborne collision avoidance system X. Tech. rep., Massachusetts Institute of Technology-Lincoln Laboratory Lexington United States."},{"key":"6065_CR31","doi-asserted-by":"crossref","unstructured":"Owen, M.P., Panken, A., Moss, R., Alvarez, L., & Leeper, C. (2019). ACAS Xu: Integrated collision avoidance and detect and avoid capability for UAS. In IEEE\/AIAA digital avionics systems conference (DASC), pp 1\u201310.","DOI":"10.1109\/DASC43569.2019.9081758"},{"key":"6065_CR32","doi-asserted-by":"crossref","unstructured":"Pan, Y., Cheng, C.A., Saigol, K., Lee, K., Yan, X., Theodorou, E., & Boots, B. (2017). Agile autonomous driving using end-to-end deep imitation learning. arXiv preprint arXiv:170907174.","DOI":"10.15607\/RSS.2018.XIV.056"},{"key":"6065_CR33","unstructured":"Sidrane, C., & Kochenderfer, M.J. (2019). OVERT: Verification of nonlinear dynamical systems with neural network controllers via overapproximation. In Workshop on safe machine learning, international conference on learning representations."},{"key":"6065_CR34","unstructured":"Tjeng, V., Xiao, K., & Tedrake, R. (2017). Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:171107356."},{"key":"6065_CR35","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., & Jana, S. (2018). Formal security analysis of neural networks using symbolic intervals. In USENIX security symposium., pp 1599\u20131614, https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi."},{"key":"6065_CR36","unstructured":"Xiang, W., & Johnson, T.T. (2018). Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:180509944."},{"key":"6065_CR37","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H.D., Rosenfeld, J.A., & Johnson, T.T. (2018). Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In American control conference, pp 1574\u20131579.","DOI":"10.23919\/ACC.2018.8431048"},{"key":"6065_CR38","doi-asserted-by":"crossref","unstructured":"Xiang, W., Lopez, D.M., Musau, P., & Johnson, T.T. (2019). Reachable set estimation and verification for neural network models of nonlinear dynamic systems. In Safe, autonomous and intelligent vehicles. Springer, pp 123\u2013144.","DOI":"10.1007\/978-3-319-97301-2_7"}],"container-title":["Machine Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-021-06065-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10994-021-06065-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-021-06065-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T21:03:26Z","timestamp":1691096606000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10994-021-06065-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,19]]},"references-count":38,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["6065"],"URL":"https:\/\/doi.org\/10.1007\/s10994-021-06065-9","relation":{},"ISSN":["0885-6125","1573-0565"],"issn-type":[{"value":"0885-6125","type":"print"},{"value":"1573-0565","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,19]]},"assertion":[{"value":"22 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 July 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 September 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 October 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflicts of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}