{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:52:22Z","timestamp":1756000342740,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031684159"},{"type":"electronic","value":"9783031684166"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-68416-6_15","type":"book-chapter","created":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:02:40Z","timestamp":1724828560000},"page":"249-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["IMPaCT: Interval MDP Parallel Construction for\u00a0Controller Synthesis of\u00a0Large-Scale STochastic Systems"],"prefix":"10.1007","author":[{"given":"Ben","family":"Wooding","sequence":"first","affiliation":[]},{"given":"Abolfazl","family":"Lavaei","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,29]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., et\u00a0al.: ARCH-COMP23 category report: stochastic models. In: International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC Series in Computing, pp. 126\u2013150. EasyChair (2023)","DOI":"10.29007\/k7s6"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.29007\/lsvc","volume":"90","author":"A Abate","year":"2022","unstructured":"Abate, A., et al.: ARCH-COMP22 category report: stochastic models. EPiC Ser. Comput. 90, 113\u2013141 (2022)","journal-title":"EPiC Ser. Comput."},{"issue":"11","key":"15_CR3","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"key":"15_CR4","unstructured":"Abate, A., et al.: ARCH-COMP20 Category Report: Stochastic Models (2020)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Alpay, A., Heuveline, V.: SYCL beyond OpenCL: the architecture, current state and future direction of HipSYCL. In: Proceedings of the International Workshop on OpenCL (2020)","DOI":"10.1145\/3388333.3388658"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Alpay, A., Heuveline, V.: One pass to bind them: the first single-pass SYCL compiler with unified code representation across backends. In: Proceedings of the 2023 International Workshop on OpenCL (2023)","DOI":"10.1145\/3585341.3585351"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Badings, T.S., Abate, A., Jansen, N., Parker, D., Poonawala, H.A., Stoelinga, M.: Sampling-based robust control of autonomous systems with non-gaussian noise. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 9669\u20139678 (2022)","DOI":"10.1609\/aaai.v36i9.21201"},{"key":"15_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: International Conference on Computer Aided Verification, pp. 160\u2013180 (2017)","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Belta, C., Yordanov, B., Gol, E.A.: Formal methods for discrete-time dynamical systems, vol.\u00a089 (2017)","DOI":"10.1007\/978-3-319-50763-7"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Cauchi, N., Abate, A.: StocHy: automated verification and synthesis of stochastic processes. In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019)","DOI":"10.1145\/3302504.3313349"},{"issue":"7","key":"15_CR12","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.ipl.2013.01.004","volume":"113","author":"T Chen","year":"2013","unstructured":"Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210\u2013216 (2013)","journal-title":"Inf. Process. Lett."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Delimpaltadakis, G., Lahijanian, M., Mazo, M., Laurenti, L.: Interval Markov decision processes with continuous action-spaces. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2023)","DOI":"10.1145\/3575870.3587117"},{"issue":"7","key":"15_CR14","doi-asserted-by":"publisher","first-page":"2975","DOI":"10.1109\/TAC.2020.3014142","volume":"66","author":"M Dutreix","year":"2020","unstructured":"Dutreix, M., Coogan, S.: Specification-guided verification and abstraction refinement of mixed monotone stochastic systems. IEEE Trans. Autom. Control 66(7), 2975\u20132990 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: 8th International Workshop on Reachability Problems, pp. 125\u2013137 (2014)","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"15_CR18","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Hashemi, V., Hermanns, H., Song, L., Subramani, K., Turrini, A., Wojciechowski, P.: Compositional bisimulation minimization for interval Markov decision processes. In: 10th International Conference on Language and Automata Theory and Applications, pp. 114\u2013126 (2016)","DOI":"10.1007\/978-3-319-30000-9_9"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"2641","DOI":"10.1109\/LCSYS.2022.3173993","volume":"6","author":"J Jiang","year":"2022","unstructured":"Jiang, J., Zhao, Y., Coogan, S.: Safe learning for uncertainty-aware planning via interval MDP abstraction. IEEE Control Syst. Lett. 6, 2641\u20132646 (2022)","journal-title":"IEEE Control Syst. Lett."},{"key":"15_CR21","unstructured":"Johnson, S.G.: The NLopt nonlinear-optimization package (2007). https:\/\/github.com\/stevengj\/nlopt"},{"issue":"6","key":"15_CR22","doi-asserted-by":"publisher","first-page":"1193","DOI":"10.1109\/TAC.2009.2019791","volume":"54","author":"AA Julius","year":"2009","unstructured":"Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Trans. Autom. Control 54(6), 1193\u20131203 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"key":"15_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61871-1","volume-title":"Foundations of Modern Probability","author":"O Kallenberg","year":"2021","unstructured":"Kallenberg, O.: Foundations of Modern Probability, vol. 3. Springer, Cham (2021)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Khaled, M., Zamani, M.: PFaces: an acceleration ecosystem for symbolic control. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 252\u2013257 (2019)","DOI":"10.1145\/3302504.3311798"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: 23rd International Conference on Computer Aided Verification, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"8","key":"15_CR26","doi-asserted-by":"publisher","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"M Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60(8), 2031\u20132045 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-53291-8_24","volume-title":"Computer Aided Verification","author":"A Lavaei","year":"2020","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.) CAV 2020. LNCS, vol. 12225, pp. 461\u2013474. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_24"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. Automatica 146 (2022)","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"15_CR29","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1109\/LCSYS.2022.3188535","volume":"7","author":"A Lavaei","year":"2022","unstructured":"Lavaei, A., Soudjani, S., Frazzoli, E., Zamani, M.: Constructing MDP abstractions using data with formal guarantees. IEEE Control Syst. Lett. 7, 460\u2013465 (2022)","journal-title":"IEEE Control Syst. Lett."},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Zamani, M.: From dissipativity theory to compositional construction of finite Markov decision processes. In: Proceedings of the 21st ACM International Conference on Hybrid Systems: Computation and Control, pp. 21\u201330 (2018)","DOI":"10.1145\/3178126.3178135"},{"key":"15_CR31","unstructured":"Makhorin, A.: GLPK (GNU linear programming kit) (2008). http:\/\/www.gnu.org\/s\/glpk\/glpk.html"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Mathiesen, F.B., Lahijanian, M., Laurenti, L.: IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes (2024)","DOI":"10.1016\/j.ifacol.2024.07.416"},{"key":"15_CR33","unstructured":"Rickard, L., Abate, A., Margellos, K.: Learning robust policies for uncertain parametric Markov decision processes. arXiv: 2312.06344 (2023)"},{"key":"15_CR34","unstructured":"Rowan, T.H.: Functional stability analysis of numerical algorithms. Ph.D. thesis, Department of Computer Science, University of Texas at Austin (1990)"},{"issue":"2","key":"15_CR35","doi-asserted-by":"publisher","first-page":"26","DOI":"10.21105\/joss.00026","volume":"1","author":"C Sanderson","year":"2016","unstructured":"Sanderson, C., Curtin, R.: Armadillo: a template-based C++ library for linear algebra. J. Open Source Softw. 1(2), 26 (2016)","journal-title":"J. Open Source Softw."},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Sanderson, C., Curtin, R.: A user-friendly hybrid sparse matrix class in C++. In: 6th International Conference on Mathematical Software, pp. 422\u2013430 (2018)","DOI":"10.1007\/978-3-319-96418-8_50"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: 12th International Conference Tools and Algorithms for the Construction and Analysis of Systems, pp. 394\u2013410 (2006)","DOI":"10.1007\/11691372_26"},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-662-46681-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SEZ Soudjani","year":"2015","unstructured":"Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST$$^{\\sf 2}$$: formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272\u2013286. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_23"},{"key":"15_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Cham (2009)"},{"key":"15_CR40","unstructured":"The HDF Group: Hierarchical Data Format, version 5 (1997\u20132023). https:\/\/www.hdfgroup.org\/HDF5\/"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.P., Abate, A.: Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In: Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control, pp. 293\u2013302 (2013)","DOI":"10.1145\/2461328.2461373"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Van\u00a0Huijgevoort, B., Sch\u00f6n, O., Soudjani, S., Haesaert, S.: SySCoRe: synthesis via stochastic coupling relations. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2023)","DOI":"10.1145\/3575870.3587123"},{"key":"15_CR43","doi-asserted-by":"crossref","unstructured":"Weininger, M., Meggendorfer, T., K\u0159et\u00ednsk\u1ef3, J.: Satisfiability bounds for $$\\omega $$-regular properties in bounded-parameter Markov decision processes. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 2284\u20132291 (2019)","DOI":"10.1109\/CDC40024.2019.9029460"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Wooding, B., Lavaei, A.: IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems (2024)","DOI":"10.1007\/978-3-031-68416-6_15"},{"issue":"12","key":"15_CR45","doi-asserted-by":"publisher","first-page":"3135","DOI":"10.1109\/TAC.2014.2351652","volume":"59","author":"M Zamani","year":"2014","unstructured":"Zamani, M., Mohajerin Esfahani, P., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 3135\u20133150 (2014)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-68416-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T10:28:51Z","timestamp":1732703331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-68416-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031684159","9783031684166"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-68416-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Calgary, AB","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}