{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:37:01Z","timestamp":1775684221961,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030317836","type":"print"},{"value":"9783030317843","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31784-3_5","type":"book-chapter","created":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T21:32:04Z","timestamp":1571607124000},"page":"81-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Jaeger","sequence":"first","affiliation":[]},{"given":"Peter Gj\u00f8l","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Guldstrand Larsen","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[]},{"given":"Jakob Haahr","family":"Taankvist","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"issue":"1\u20132","key":"5_CR1","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(94)00011-O","volume":"72","author":"AG Barto","year":"1995","unstructured":"Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artif. Intell. 72(1\u20132), 81\u2013138 (1995). \nhttps:\/\/doi.org\/10.1016\/0004-3702(94)00011-O\n\n. ISSN 0004\u20133702","journal-title":"Artif. Intell."},{"key":"5_CR2","unstructured":"Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees (1984)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods: Performance Modeling and Verification","author":"PR D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57\u201376. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45605-8_5"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A David","year":"2011","unstructured":"David, A., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80\u201396. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24310-3_7"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2014","unstructured":"David, A., et al.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129\u2013145. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6_10"},{"key":"5_CR6","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). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397\u2013415 (2015). \nhttps:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"STTT"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: QEST 2012, pp. 84\u201393 (2012). \nhttps:\/\/doi.org\/10.1109\/QEST.2012.19","DOI":"10.1109\/QEST.2012.19"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST 2006, pp. 157\u2013166. IEEE Computer Society (2006). \nhttps:\/\/doi.org\/10.1109\/QEST.2006.19\n\n. ISBN 0-7695-2665-9","DOI":"10.1109\/QEST.2006.19"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-319-23506-6_17","volume-title":"Correct System Design","author":"KG Larsen","year":"2015","unstructured":"Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Safe and optimal adaptive cruise control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 260\u2013277. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23506-6_17"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-662-49674-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Miku\u010dionis, M., Mu\u00f1iz, M., Srba, J., Taankvist, J.H.: Online and compositional learning of controllers with application to floor heating. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 244\u2013259. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_14"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-030-23703-5_6","volume-title":"Cyber Physical Systems. Model-Based Design","author":"KG Larsen","year":"2019","unstructured":"Larsen, K.G., Le Co\u00ebnt, A., Miku\u010dionis, M., Taankvist, J.H.: Guaranteed control synthesis for continuous systems in Uppaal Tiga. In: Chamberlain, R., Taha, W., T\u00f6rngren, M. (eds.) CyPhy\/WESE-2018. LNCS, vol. 11615, pp. 113\u2013133. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-23703-5_6\n\n. ISBN 978-3-030-23703-5"},{"issue":"16","key":"5_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.ifacol.2018.08.016","volume":"51","author":"Yuriy Zacchia Lun","year":"2018","unstructured":"Lun, Y.Z., Wheatley, J., D\u2019Innocenzo, A., Abate, A.: Approximate abstractions of Markov chains with interval decision processes. ADHS 2018, pp. 91\u201396 (2018). \nhttps:\/\/doi.org\/10.1016\/j.ifacol.2018.08.016","journal-title":"IFAC-PapersOnLine"},{"issue":"7540","key":"5_CR15","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529 (2015)","journal-title":"Nature"},{"key":"5_CR16","unstructured":"Strehl, L. Li, A.L., Littman, M.L.: Incremental model-based learners with formal learning-time guarantees. CoRR (2012)"},{"key":"5_CR17","unstructured":"Sun, L., Guo, Y., Barbu, A.: A novel framework for online supervised learning with feature selection. arXiv e-prints, art. \narXiv:1803.11521\n\n (2018)"},{"key":"5_CR18","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press (2018)"},{"key":"5_CR19","unstructured":"Watkins, C.J.C.H.: Learning from delayed rewards. Ph.D. thesis, King\u2019s College, Cambridge (1989)"},{"issue":"3","key":"5_CR20","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1080\/00401706.1962.10490022","volume":"4","author":"BP Welford","year":"1962","unstructured":"Welford, B.P.: Note on a method for calculating corrected sums of squares and products. Technometrics 4(3), 419\u2013420 (1962). \nhttps:\/\/doi.org\/10.1080\/00401706.1962.10490022","journal-title":"Technometrics"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T13:28:45Z","timestamp":1573738125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Between 1 and 2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}