{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:42:37Z","timestamp":1759365757237,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032057914","type":"print"},{"value":"9783032057921","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-05792-1_4","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:54Z","timestamp":1759314714000},"page":"62-82","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Control for\u00a0Uncertain Systems via\u00a0Contract-Based Probabilistic Surrogates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-6455","authenticated-orcid":false,"given":"Oliver","family":"Sch\u00f6n","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4749-4688","authenticated-orcid":false,"given":"Sofie","family":"Haesaert","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-6678","authenticated-orcid":false,"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,2]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional refinement for hierarchical hybrid systems. In: Hybrid Systems: Computation and Control, pp. 33\u201348. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45351-2_7"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Annaswamy, A.M., Johansson, K.H., Pappas, G.: Control for societal-scale challenges: Road map 2030. IEEE Control Syst. Mag. 44(3), 30\u201332 (2024)","DOI":"10.1109\/MCS.2024.3382376"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Arcari, E., Iannelli, A., Carron, A., Zeilinger, M.N.: Stochastic MPC with robustness to bounded parameteric uncertainty. IEEE Trans. Autom. Control 68(12), 7601\u20137615 (2023)","DOI":"10.1109\/TAC.2023.3294868"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception contracts for safety of ML-enabled systems. Proc. ACM Program. Lang. 7(OOPSLA2) (2023)","DOI":"10.1145\/3622875"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Badings, T., Romao, L., Abate, A., Jansen, N.: Probabilities are not enough: formal controller synthesis for stochastic dynamical models with epistemic uncertainty. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, no. 12, pp. 14701\u201314710 (2023)","DOI":"10.1609\/aaai.v37i12.26718"},{"key":"4_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Banse, A., Romao, L., Abate, A., Jungers, R.M.: Data-driven abstractions via adaptive refinements and a Kantorovich metric. In: 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 6038\u20136043 (2023)","DOI":"10.1109\/CDC49753.2023.10383513"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Belta, C.: Formal synthesis of control strategies for dynamical systems. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 3407\u20133431 (2016)","DOI":"10.1109\/CDC.2016.7798782"},{"key":"4_CR9","unstructured":"Bengio, Y., et al.: International scientific report on the safety of advanced AI. Technical report, Department for Science, Innovation and Technology (2024)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Bogachev, V.I.: Measure Theory. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-34514-5"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-662-45489-3_3","volume-title":"Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems","author":"CE Budde","year":"2014","unstructured":"Budde, C.E., D\u2019Argenio, P.R., S\u00e1nchez Terraf, P., Wolovick, N.: A theory for the semantics of stochastic and non-deterministic continuous systems. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. LNCS, vol. 8453, pp. 67\u201386. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-45489-3_3"},{"key":"4_CR12","unstructured":"Casablanca, E., Zhang, Z., Marchesini, G., Haesaert, S., Dimarogonas, D.V., Soudjani, S.: SymAware: a software development framework for trustworthy multi-agent systems with situational awareness. arXiv preprint arXiv:2409.14833 (2024)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-63501-9_8","volume-title":"Numerical Software Verification","author":"Y Chou","year":"2017","unstructured":"Chou, Y., Chen, X., Sankaranarayanan, S.: A study of model-order reduction techniques for verification. In: Abate, A., Boldo, S. (eds.) NSV 2017. LNCS, vol. 10381, pp. 98\u2013113. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63501-9_8"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Coppola, R., Peruffo, A., Romao, L., Abate, A., Mazo, M.: Enhancing data-driven stochastic control via bundled interval MDP. IEEE Control Syst. Lett. (2024)","DOI":"10.1109\/LCSYS.2024.3417852"},{"key":"4_CR15","unstructured":"Dalrymple, D., et\u00a0al.: Towards guaranteed safe AI: a framework for ensuring robust and reliable AI systems. arXiv preprint arXiv:2405.06624 (2024)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163\u2013193 (2002)","DOI":"10.1006\/inco.2001.2962"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating labelled Markov processes. Inf. Comput. 184(1), 160\u2013200 (2003)","DOI":"10.1016\/S0890-5401(03)00051-8"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Edalat, A.: Semi-pullbacks and bisimulation in categories of Markov processes. Math. Struct. Comput. Sci. 9(5), 523\u2013543 (1999)","DOI":"10.1017\/S0960129599002819"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Ghasemi, K., Sadraddini, S., Belta, C.: Compositional synthesis via a convex parameterization of assume-guarantee contracts. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2020)","DOI":"10.1145\/3365365.3382212"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Gracia, I., Boskos, D., Laurenti, L., Mazo\u00a0Jr, M.: Distributionally robust strategy synthesis for switched stochastic systems. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2023)","DOI":"10.1145\/3575870.3587127"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1024","DOI":"10.1109\/TAC.2020.2992443","volume":"66","author":"S Haesaert","year":"2021","unstructured":"Haesaert, S., Chen, F., Abate, A., Weiland, S.: Formal control synthesis via simulation relations and behavioral theory for discrete-time descriptor systems. IEEE Trans. Autom. Control 66(3), 1024\u20131039 (2021)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Haesaert, S., Soudjani, S., Abate, A.: Verification of general Markov decision processes by approximate similarity relations and policy refinement. SIAM J. Control. Optim. 55(4), 2333\u20132367 (2017)","DOI":"10.1137\/16M1079397"},{"issue":"2","key":"4_CR23","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":"4_CR24","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Lahijanian, M., Turrini, A.: Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves. ACM Trans. Model. Comput. Simul. (TOMACS) 29(4), 1\u201331 (2019)","DOI":"10.1145\/3309683"},{"key":"4_CR25","unstructured":"Jafarpour, S., Chen, Y.: Probabilistic reachability of stochastic control systems: a contraction-based approach. arXiv preprint arXiv:2407.12225 (2024)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Kazemi, M., Perez, M., Somenzi, F., Soudjani, S., Trivedi, A., Velasquez, A.: Assume-guarantee reinforcement learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a038, pp. 21223\u201321231 (2024)","DOI":"10.1609\/aaai.v38i19.30116"},{"issue":"3","key":"4_CR27","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23\u201337. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_3"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1109\/OJCSYS.2023.3329394","volume":"2","author":"A Lavaei","year":"2023","unstructured":"Lavaei, A., et al.: Compositional reinforcement learning for discrete-time stochastic control systems. IEEE Open J. Control Syst. 2, 425\u2013438 (2023)","journal-title":"IEEE Open J. Control Syst."},{"key":"4_CR30","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110617","volume":"146","author":"A Lavaei","year":"2022","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. Automatica 146, 110617 (2022)","journal-title":"Automatica"},{"issue":"2","key":"4_CR31","first-page":"278","volume":"237","author":"M Luckcuck","year":"2023","unstructured":"Luckcuck, M.: Using formal methods for autonomous systems: five recipes for formal verification. Proc. Inst. Mech. Engineers Part O: J. Risk Reliabil. 237(2), 278\u2013292 (2023)","journal-title":"Proc. Inst. Mech. Engineers Part O: J. Risk Reliabil."},{"issue":"6","key":"4_CR32","doi-asserted-by":"publisher","first-page":"2629","DOI":"10.1109\/TAC.2018.2869740","volume":"64","author":"K Mallik","year":"2018","unstructured":"Mallik, K., Schmuck, A.K., Soudjani, S., Majumdar, R.: Compositional synthesis of finite-state abstractions. IEEE Trans. Autom. Control 64(6), 2629\u20132636 (2018)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"4_CR33","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/MCS.2024.3382388","volume":"44","author":"N Matni","year":"2024","unstructured":"Matni, N., Ames, A.D., Doyle, J.C.: A quantitative framework for layered multirate control: toward a theory of control architecture. IEEE Control Syst. Mag. 44(3), 52\u201394 (2024)","journal-title":"IEEE Control Syst. Mag."},{"key":"4_CR34","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1109\/OJCSYS.2023.3305835","volume":"2","author":"SP Nayak","year":"2023","unstructured":"Nayak, S.P., Egidio, L.N., Della Rossa, M., Schmuck, A.K., Jungers, R.M.: Context-triggered abstraction-based control design. IEEE Open J. Control Syst. 2, 277\u2013296 (2023)","journal-title":"IEEE Open J. Control Syst."},{"issue":"1","key":"4_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3243216","volume":"18","author":"P Nuzzo","year":"2019","unstructured":"Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., Xi, Y., Li, D.: Stochastic assume-guarantee contracts for cyber-physical system design. ACM Trans. Embed. Comput. Syst. (TECS) 18(1), 1\u201326 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"P\u0103s\u0103reanu, C.S., et al.: Closed-loop analysis of vision-based autonomous systems: a case study. In: International Conference on Computer Aided Verification, pp. 289\u2013303. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_15","DOI":"10.1007\/978-3-031-37706-8_15"},{"issue":"1","key":"4_CR37","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MITP.2024.3356158","volume":"26","author":"G Provan","year":"2024","unstructured":"Provan, G.: Formal methods for autonomous vehicles. IT Prof. 26(1), 50\u201356 (2024)","journal-title":"IT Prof."},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Pulch, R.: 10 Model Order Reduction in Uncertainty Quantification, pp. 321\u2013344. De Gruyter, Berlin (2021)","DOI":"10.1515\/9783110499001-010"},{"key":"4_CR39","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Hoboken (2014)"},{"key":"4_CR40","unstructured":"Sch\u00f6n, O., Haesaert, S., Soudjani, S.: Formal control for uncertain systems via contract-based probabilistic surrogates (extended version). arXiv preprint (2025)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Sch\u00f6n, O., van Huijgevoort, B., Haesaert, S., Soudjani, S.: Verifying the unknown: correct-by-design control synthesis for networks of stochastic uncertain systems. In: 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 7035\u20137042. IEEE (2023)","DOI":"10.1109\/CDC49753.2023.10383307"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Sch\u00f6n, O., van Huijgevoort, B., Haesaert, S., Soudjani, S.: Bayesian formal synthesis of unknown systems via robust simulation relations. IEEE Trans. Autom. Control (2024)","DOI":"10.1109\/TAC.2024.3459308"},{"issue":"2","key":"4_CR43","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nordic J. Comput."},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Shali, B.M., Heidema, H.M., van\u00a0der Schaft, A.J., Besselink, B.: Series composition of simulation-based assume-guarantee contracts for linear dynamical systems. In: 2022 IEEE 61st Conference on Decision and Control (CDC), pp. 2204\u20132209 (2022)","DOI":"10.1109\/CDC51059.2022.9992487"},{"issue":"2","key":"4_CR45","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Soudjani","year":"2013","unstructured":"Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2013)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"4_CR46","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, Boston (2009)"},{"key":"4_CR47","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":"4_CR48","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110476","volume":"144","author":"BC van Huijgevoort","year":"2022","unstructured":"van Huijgevoort, B.C., Haesaert, S.: Similarity quantification for linear stochastic systems: a coupling compensator approach. Automatica 144, 110476 (2022)","journal-title":"Automatica"},{"key":"4_CR49","unstructured":"Wang, R., Sun, Z., Haesaert, S.: Unraveling tensor structures in correct-by-design controller synthesis. arXiv preprint arXiv:2503.24085 (2025)"},{"key":"4_CR50","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2024.100940","volume":"57","author":"X Yin","year":"2024","unstructured":"Yin, X., Gao, B., Yu, X.: Formal synthesis of controllers for safety-critical autonomous systems: developments and challenges. Ann. Rev. Control. 57, 100940 (2024)","journal-title":"Ann. Rev. Control."},{"key":"4_CR51","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110696","volume":"147","author":"B Zhong","year":"2023","unstructured":"Zhong, B., Lavaei, A., Zamani, M., Caccamo, M.: Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations. Automatica 147, 110696 (2023)","journal-title":"Automatica"}],"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-032-05792-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:32:06Z","timestamp":1759314726000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05792-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,2]]},"ISBN":["9783032057914","9783032057921"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05792-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,2]]},"assertion":[{"value":"2 October 2025","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":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","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":"26 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2025","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"}}]}}