{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T10:08:46Z","timestamp":1769854126848,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T00:00:00Z","timestamp":1746489600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,5,6]]},"DOI":"10.1145\/3716863.3718031","type":"proceedings-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:20:33Z","timestamp":1747808433000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Scalable control synthesis for stochastic systems via structural IMDP abstractions"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2243-0445","authenticated-orcid":false,"given":"Frederik Baymler","family":"Mathiesen","sequence":"first","affiliation":[{"name":"Delft University of Technology, Delft, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4749-4688","authenticated-orcid":false,"given":"Sofie","family":"Haesaert","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1190-6097","authenticated-orcid":false,"given":"Luca","family":"Laurenti","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Delft, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,5,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Alessandro Abate H.A.P. Blom Nathalie Cauchi Joanna Delicaris Arnd Hartmanns Mahmoud Khaled Abolfazl Lavaei Carina Pilch Anne Remke and More Authors. 2020. ARCH-COMP20 Category Report: Stochastic Models. In EPiC Series in Computing."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2022.3178143"},{"key":"e_1_3_2_1_4_1","volume-title":"Finite Neural Networks as Mixtures of Gaussian Processes: From Provable Error Bounds to Prior Selection. arXiv e-prints","author":"Adams Steven","year":"2024","unstructured":"Steven Adams, Andrea Patane, Morteza Lahijanian, and Luca Laurenti. 2024. Finite Neural Networks as Mixtures of Gaussian Processes: From Provable Error Bounds to Prior Selection. arXiv e-prints (2024), arXiv-2407."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.14253"},{"key":"e_1_3_2_1_6_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_3_2_1_7_1","volume-title":"Stochastic Optimal Control: the Discrete-time Case","author":"Bertsekas Dimitri P","unstructured":"Dimitri P Bertsekas and Steven E Shreve. 2004. Stochastic Optimal Control: the Discrete-time Case. Athena Scientific."},{"key":"e_1_3_2_1_8_1","volume-title":"Julia: A fast dynamic language for technical computing. arXiv preprint arXiv:1209.5145","author":"Bezanson Jeff","year":"2012","unstructured":"Jeff Bezanson, Stefan Karpinski, Viral B Shah, and Alan Edelman. 2012. Julia: A fast dynamic language for technical computing. arXiv preprint arXiv:1209.5145 (2012)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00033-3"},{"key":"e_1_3_2_1_10_1","volume-title":"12th international symposium on advanced vehicle control","volume":"9","author":"Carvalho Ashwin","year":"2014","unstructured":"Ashwin Carvalho, Yiqi Gao, St\u00e9phanie Lefevre, and Francesco Borrelli. 2014. Stochastic predictive control of autonomous vehicles in uncertain environments. In 12th international symposium on advanced vehicle control, Vol. 9."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311805"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_22"},{"key":"e_1_3_2_1_13_1","volume-title":"Formal Methods for Trusted Space Autonomy: Boon or Bane?","author":"Chien Steve A.","unstructured":"Steve A. Chien. 2022. Formal Methods for Trusted Space Autonomy: Boon or Bane?. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham, 3--13."},{"key":"e_1_3_2_1_14_1","volume-title":"Introduction to Algorithms (2 ed.)","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2001. Introduction to Algorithms (2 ed.). The MIT Press."},{"key":"e_1_3_2_1_15_1","unstructured":"Delft High Performance Computing Centre. 2024. DelftBlue Supercomputer (Phase 2). https:\/\/www.tudelft.nl\/dhpc\/ark:\/44463\/DelftBluePhase2."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0287-9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(00)00047-3"},{"key":"e_1_3_2_1_18_1","volume-title":"Holger Hermanns, and Khaled Elbassioni.","author":"Hashemi Vahid","year":"2017","unstructured":"Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, and Khaled Elbassioni. 2017. Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. In Dependable Software Engineering. Theories, Tools, and Applications, Kim Guldstrand Larsen, Oleg Sokolsky, and Ji Wang (Eds.). Springer International Publishing, Cham, 25--41."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"e_1_3_2_1_20_1","volume-title":"Towards Data-driven Verification of Unknown Dynamical Systems. In 2nd RSS Workshop on Robust Autonomy: Tools for Safety in Real-World Uncertain Environments (RSS","author":"Jackson John","year":"2020","unstructured":"John Jackson, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2020. Towards Data-driven Verification of Unknown Dynamical Systems. In 2nd RSS Workshop on Robust Autonomy: Tools for Safety in Real-World Uncertain Environments (RSS 2020)."},{"key":"e_1_3_2_1_21_1","volume-title":"Formal verification of unknown dynamical systems via Gaussian process regression. arXiv preprint arXiv:2201.00655","author":"Jackson John","year":"2021","unstructured":"John Jackson, Luca Laurenti, Eric Frew, and Morteza Lahijanian. 2021. Formal verification of unknown dynamical systems via Gaussian process regression. arXiv preprint arXiv:2201.00655 (2021)."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2022.3173993"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_2_1_24_1","unstructured":"Morteza Lahijanian. 2021. bmdp-tool. https:\/\/github.com\/aria-systems-group\/bmdp-tool Standalone software."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2398883"},{"key":"e_1_3_2_1_26_1","volume-title":"Unifying Safety Approaches for Stochastic Systems: From Barrier Functions to Uncertain Abstractions via Dynamic Programming. arXiv preprint arXiv:2310.01802","author":"Laurenti Luca","year":"2023","unstructured":"Luca Laurenti and Morteza Lahijanian. 2023. Unifying Safety Approaches for Stochastic Systems: From Barrier Functions to Uncertain Abstractions via Dynamic Programming. arXiv preprint arXiv:2310.01802 (2023)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.2975028"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2020.100991"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Changliu Liu Tomer Arnon Christopher Lazarus Christopher Strong Clark Barrett Mykel J Kochenderfer et al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends in Optimization (2021).","DOI":"10.1561\/9781680837872"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562137"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907293"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2022.3229865"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Frederik Baymler Mathiesen Sofie Haesaert and Luca Laurenti. 2025. Scalable control synthesis for stochastic systems via structural IMDP abstractions. arXiv:2411.11803 [eess.SY] https:\/\/arxiv.org\/abs\/2411.11803","DOI":"10.1145\/3716863.3718031"},{"key":"e_1_3_2_1_35_1","unstructured":"Frederik Baymler Mathiesen Morteza Lahijanian and Luca Laurenti. 2024. IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes. arXiv:2401.04068 [eess.SY] https:\/\/arxiv.org\/abs\/2401.04068"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC49753.2023.10383306"},{"key":"e_1_3_2_1_37_1","volume-title":"Luca Laurenti, and Morteza Lahijanian.","author":"Mazouz Rayan","year":"2024","unstructured":"Rayan Mazouz, Frederik Baymler Mathiesen, Luca Laurenti, and Morteza Lahijanian. 2024. Piecewise Stochastic Barrier Functions. arXiv:2404.16986 [cs.RO] https:\/\/arxiv.org\/abs\/2404.16986"},{"key":"e_1_3_2_1_38_1","first-page":"9672","article-title":"Safety guarantees for neural network dynamic systems via stochastic barrier functions","volume":"35","author":"Mazouz Rayan","year":"2022","unstructured":"Rayan Mazouz, Karan Muvvala, Akash Ratheesh Babu, Luca Laurenti, and Morteza Lahijanian. 2022. Safety guarantees for neural network dynamic systems via stochastic barrier functions. Advances in Neural Information Processing Systems 35 (2022), 9672--9686.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_39_1","volume-title":"Universal series induced by approximate identities and some relevant applications. Journal of Approximation Theory","author":"Nestoridis Vassili","year":"2011","unstructured":"Vassili Nestoridis, Sebastian Schmutzhard, and Vangelis Stefanopoulos. 2011. Universal series induced by approximate identities and some relevant applications. Journal of Approximation Theory (2011)."},{"key":"e_1_3_2_1_40_1","volume-title":"Ali-Akbar Agha-Mohammadi, Richard M Murray, and Aaron D Ames.","author":"Nilsson Petter","year":"2018","unstructured":"Petter Nilsson, Sofie Haesaert, Rohan Thakker, Kyohei Otsu, Cristian Ioan Vasile, Ali-Akbar Agha-Mohammadi, Richard M Murray, and Aaron D Ames. 2018. Toward Specification-Guided Active Mars Exploration for Cooperative Robot Teams.. In Robotics: Science and systems, Vol. 14. 1--9."},{"key":"e_1_3_2_1_41_1","first-page":"1","article-title":"Adversarial robustness guarantees for gaussian processes","volume":"23","author":"Patane Andrea","year":"2022","unstructured":"Andrea Patane, Arno Blaas, Luca Laurenti, Luca Cardelli, Stephen Roberts, and Marta Kwiatkowska. 2022. Adversarial robustness guarantees for gaussian processes. Journal of Machine Learning Research 23, 146 (2022), 1--55.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2023.3340995"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2021.08.466"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2020.109439"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2023.3340621"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2014.2358844"},{"key":"e_1_3_2_1_48_1","volume-title":"Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday","author":"Suilen Marnix","unstructured":"Marnix Suilen, Thom Badings, Eline M Bovy, David Parker, and Nils Jansen. 2024. Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet. In Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III. Springer, 126--154."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575870.3587123"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110476"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","unstructured":"B. C. van Huijgevoort S. Weiland and S. Haesaert. 2023. Temporal Logic Control of Nonlinear Stochastic Systems Using a Piecewise-Affine Abstraction. IEEE Control Systems Letters (2023). doi:10.1109\/LCSYS.2022.3230765","DOI":"10.1109\/LCSYS.2022.3230765"},{"key":"e_1_3_2_1_52_1","volume-title":"Gaussian processes for regression. Advances in neural information processing systems 8","author":"Williams Christopher","year":"1995","unstructured":"Christopher Williams and Carl Rasmussen. 1995. Gaussian processes for regression. Advances in neural information processing systems 8 (1995)."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Ben Wooding and Abolfazl Lavaei. 2024. IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale STochastic Systems. In Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems.","DOI":"10.1007\/978-3-031-68416-6_15"}],"event":{"name":"HSCC '25: Computation and Control","location":"Irvine CA USA","acronym":"HSCC '25","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716863.3718031","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716863.3718031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:46:40Z","timestamp":1756993600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716863.3718031"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,6]]},"references-count":53,"alternative-id":["10.1145\/3716863.3718031","10.1145\/3716863"],"URL":"https:\/\/doi.org\/10.1145\/3716863.3718031","relation":{},"subject":[],"published":{"date-parts":[[2025,5,6]]},"assertion":[{"value":"2025-05-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}