{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T11:07:42Z","timestamp":1784286462344,"version":"3.55.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032323569","type":"print"},{"value":"9783032323576","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T00:00:00Z","timestamp":1784332800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T00:00:00Z","timestamp":1784332800000},"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":[[2027]]},"DOI":"10.1007\/978-3-032-32357-6_12","type":"book-chapter","created":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T10:35:55Z","timestamp":1784284555000},"page":"254-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Faster Optimization of\u00a0Decision Tree Policies for\u00a0Markov Decision Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2547-9858","authenticated-orcid":false,"given":"Dani\u00ebl","family":"Vos","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9525-0333","authenticated-orcid":false,"given":"Anna","family":"Lukina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,18]]},"reference":[{"key":"12_CR1","unstructured":"Andriushchenko, R., Ceska, M., Chakraborty, D., Junges, S., Kret\u00ednsk\u00fd, J., Mac\u00e1k, F.: Symbiotic local search for small decision tree policies in MDPs. In: Chiappa, S., Magliacane, S. (eds.) UAI, Proceedings of Machine Learning Research, PMLR, pp. 132\u2013148 (2025). https:\/\/proceedings.mlr.press\/v286\/andriushchenko25a.html"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Mac\u00e1k, F.: Policies grow on trees: model checking families of MDPs. In: ATVA 2024. LNCS, pp. 51\u201375. Springer (2024)","DOI":"10.1007\/978-3-031-78750-8_3"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Mac\u00e1k, F.: Small decision trees for MDPs with deductive synthesis. In: Piskac, R., Rakamaric, Z. (eds.) CAV. LNCS, pp. 169\u2013192. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_8","DOI":"10.1007\/978-3-031-98679-6_8"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1613\/jair.1.16593","volume":"82","author":"R Andriushchenko","year":"2025","unstructured":"Andriushchenko, R., Ceska, M., Mac\u00e1k, F., Junges, S., Katoen, J.: An oracle-guided approach to constrained policy synthesis under uncertainty. J. Artif. Intell. Res. 82, 433\u2013469 (2025)","journal-title":"J. Artif. Intell. Res."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Ashok, P., Jackermeier, M., Jagtap, P., Kret\u00ednsk\u00fd, J., Weininger, M., Zamani, M.: dtControl: decision tree learning algorithms for controller representation. In: HSCC, pp. 17:1\u201317:7. ACM (2020)","DOI":"10.1145\/3365365.3382220"},{"key":"12_CR6","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":"12_CR7","doi-asserted-by":"crossref","unstructured":"Azeem, M., et al.: 1-2-3-Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: VMCAI 2025. LNCS, pp. 97\u2013120. Springer (2025)","DOI":"10.1007\/978-3-031-82703-7_5"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories (2021)","DOI":"10.3233\/FAIA201017"},{"key":"12_CR9","unstructured":"Bastani, O., Pu, Y., Solar-Lezama, A.: Verifiable reinforcement learning via policy extraction. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) NeurIPS, pp. 2499\u20132509 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/e6d8545daa42d5ced125a4bf747b3688-Abstract.html"},{"issue":"5","key":"12_CR10","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6(5), 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Fellner, A., Kret\u00ednsk\u00fd, J.: Counterexample explanation by learning small strategies in Markov Decision Processes. In: CAV 2015. LNCS, pp. 158\u2013177. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_10"},{"key":"12_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":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J., Volk, M.: A storm is coming: a modern probabilistic model checker. In: CAV 2017. LNCS, pp. 592\u2013600. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Demirovic, E., Schilling, C., Lukina, A.: In search of trees: decision-tree policy synthesis for black-box systems via search. In: Walsh, T., Shah, J., Kolter, Z. (eds.) AAAI, pp. 27250\u201327257. AAAI Press (2025). https:\/\/doi.org\/10.1609\/AAAI.V39I26.34934","DOI":"10.1609\/AAAI.V39I26.34934"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press (2015)","DOI":"10.7551\/mitpress\/10187.001.0001"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Computer Performance Evaluation \/ TOOLS. LNCS, pp. 200\u2013204. Springer (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"12_CR19","unstructured":"van\u00a0der Linden, J.G.M., de\u00a0Weerdt, M., Demirovic, E.: Necessary and sufficient conditions for optimal decision trees using dynamic programming. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) NeurIPS (2023). http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/1d5fce9627e15c84db572a66e029b1fc-Abstract-Conference.html"},{"issue":"3","key":"12_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/3236386.3241340","volume":"16","author":"ZC Lipton","year":"2018","unstructured":"Lipton, Z.C.: The mythos of model interpretability: in machine learning, the concept of interpretability is both important and slippery. Queue 16(3), 31\u201357 (2018)","journal-title":"Queue"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Pedregosa, F., et al.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825\u20132830 (2011). https:\/\/doi.org\/10.5555\/1953048.2078195","DOI":"10.5555\/1953048.2078195"},{"issue":"5","key":"12_CR22","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1038\/s42256-019-0048-x","volume":"1","author":"C Rudin","year":"2019","unstructured":"Rudin, C.: Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nat. Mach. Intell. 1(5), 206\u2013215 (2019)","journal-title":"Nat. Mach. Intell."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Schilling, C., Lukina, A., Demirovic, E., Larsen, K.G.: Safety verification of decision-tree policies in continuous time. In: NeurIPS (2023)","DOI":"10.52202\/075280-0650"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Topin, N., Milani, S., Fang, F., Veloso, M.: Iterative bounding MDPs: learning interpretable policies via non-interpretable methods. In: AAAI 2021, pp. 9923\u20139931. AAAI Press (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I11.17192","DOI":"10.1609\/AAAI.V35I11.17192"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Vos, D., Verwer, S.: Optimal decision tree policies for Markov decision processes. In: IJCAI, pp. 5457\u20135465. ijcai.org (2023). https:\/\/doi.org\/10.24963\/IJCAI.2023\/606","DOI":"10.24963\/IJCAI.2023\/606"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32357-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T10:36:01Z","timestamp":1784284561000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32357-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,18]]},"ISBN":["9783032323569","9783032323576"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32357-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,18]]},"assertion":[{"value":"18 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/aiverification.org\/2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}