{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:33Z","timestamp":1779074613609,"version":"3.51.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032095237","type":"print"},{"value":"9783032095244","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"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-09524-4_7","type":"book-chapter","created":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:03Z","timestamp":1762290843000},"page":"97-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Uppaal Coshy: Automatic Synthesis of\u00a0Compact Shields for\u00a0Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Asger Horn","family":"Brorholt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas Holck","family":"H\u00f8eg-Petersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter Gj\u00f8l","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Schilling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Wasowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","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.) AAAI, pp. 2669\u20132678. AAAI Press (2018). https:\/\/doi.org\/10.1609\/AAAI.V32I1.11797","DOI":"10.1609\/AAAI.V32I1.11797"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Ashok, P., Jackermeier, M., Jagtap, P., Kret\u00ednsk\u00fd, J., Weininger, M., Zamani, M.: dtControl: decision tree learning algorithms for controller representation. In: Ames, A.D., Seshia, S.A., Deshmukh, J. (eds.) HSCC, pp. 17:1\u201317:7. ACM (2020). https:\/\/doi.org\/10.1145\/3365365.3382220","DOI":"10.1145\/3365365.3382220"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-030-72013-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ashok","year":"2021","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS 2021. LNCS, vol. 12652, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121\u2013125. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14"},{"issue":"3","key":"7_CR5","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1051\/ita:2002013","volume":"36","author":"J Bernet","year":"2002","unstructured":"Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. RAIRO Theor. Inf. Appl. 36(3), 261\u2013275 (2002). https:\/\/doi.org\/10.1051\/ita:2002013","journal-title":"RAIRO Theor. Inf. Appl."},{"key":"7_CR6","unstructured":"Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees. Wadsworth (1984)"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Brorholt, A.H., H\u00f8eg-Petersen, A.H., Larsen, K.G., Schilling, C.: Efficient shield synthesis via state-space transformation. In: Steffen, B. (ed.) AISoLA. LNCS, vol. 15217, pp. 206\u2013224. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_14","DOI":"10.1007\/978-3-031-75434-0_14"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Brorholt, A.H., et al.: Uppaal coshy: automatic synthesis of compact shields for hybrid systems (2025). https:\/\/arxiv.org\/abs\/2508.16345","DOI":"10.1007\/978-3-032-09524-4_7"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Brorholt, A.H., Jensen, P.G., Larsen, K.G., Lorber, F., Schilling, C.: Shielded reinforcement learning for hybrid systems. In: Steffen, B. (ed.) AISoLA. LNCS, vol. 14380, pp. 33\u201354. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_3","DOI":"10.1007\/978-3-031-46002-9_3"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 665\u2013669. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_57"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-19835-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatterjee","year":"2011","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: quantitative synthesis tool. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 267\u2013271. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_24"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.:  Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"7_CR13","unstructured":"Demirovic, E., et al.: Murtree: optimal decision trees via dynamic programming and search. J. Mach. Learn. Res. 23, 26:1\u201326:47 (2022). https:\/\/jmlr.org\/papers\/v23\/20-520.html"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Demirovi\u0107, E., Schilling, C., Lukina, A.: In search of trees: decision-tree policy synthesis for black-box systems via search. In: AAAI, pp. 27250\u201327257. AAAI Press (2025). https:\/\/doi.org\/10.1609\/aaai.v39i26.34934","DOI":"10.1609\/aaai.v39i26.34934"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1007\/978-3-319-10575-8_30","volume-title":"Handbook of Model Checking","author":"L Doyen","year":"2018","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Handbook of Model Checking, pp. 1047\u20131110. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_30"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Du, M., Liu, N., Hu, X.: Techniques for interpretable machine learning. Commun. ACM 63(1), 68\u201377 (2020). https:\/\/doi.org\/10.1145\/3359786","DOI":"10.1145\/3359786"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-030-61362-4_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"M Jaeger","year":"2020","unstructured":"Jaeger, M., Bacci, G., Bacci, G., Larsen, K.G., Jensen, P.G.: Approximating euclidean by imprecise markov decision processes. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 275\u2013289. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_15"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-31784-3_5","volume-title":"Automated Technology for Verification and Analysis","author":"M Jaeger","year":"2019","unstructured":"Jaeger, M., Jensen, P.G., Guldstrand Larsen, K., Legay, A., Sedwards, S., Taankvist, J.H.: Teaching stratego to play ball: optimal synthesis for continuous space MDPs. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 81\u201397. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_5"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-88885-5_15","volume-title":"Automated Technology for Verification and Analysis","author":"S Pranger","year":"2021","unstructured":"Pranger, S., K\u00f6nighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 222\u2013228. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_15"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Quinlan, J.R.: Learning decision tree classifiers. ACM Comput. Surv. 28(1), 71\u201372 (1996). https:\/\/doi.org\/10.1145\/234313.234346","DOI":"10.1145\/234313.234346"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2), 285\u2013309 (1955). https:\/\/www.projecteuclid.org\/journalArticle\/Download?urlId=pjm%2F1103044538","DOI":"10.2140\/pjm.1955.5.285"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-09524-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:17:46Z","timestamp":1762298266000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-09524-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"ISBN":["9783032095237","9783032095244"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-09524-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"5 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"1 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp25.software.imdea.org\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}