{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:15:20Z","timestamp":1760202920137,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030451899"},{"type":"electronic","value":"9783030451905"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_17","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"306-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-7684","authenticated-orcid":false,"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4220-3212","authenticated-orcid":false,"given":"Mateo","family":"Perez","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9093-9518","authenticated-orcid":false,"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2085-2003","authenticated-orcid":false,"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9346-0126","authenticated-orcid":false,"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5560-0546","authenticated-orcid":false,"given":"Dominik","family":"Wojtczak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"T. Babiak, M. K\u0159et\u00ednsk\u00fd, V. Reh\u00e1k, and J. Strejcek. LTL to B\u00fcchi automata translation: Fast and more deterministic. In Tools and Algorithms for the Construction and Analysis of Systems, pages 95\u2013109, 2012.","key":"17_CR1","DOI":"10.1007\/978-3-642-28756-5_8"},{"unstructured":"Ch. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.","key":"17_CR2"},{"doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Foundations of Computer Science, pages 338\u2013345. IEEE, 1988.","key":"17_CR3","DOI":"10.1109\/SFCS.1988.21950"},{"doi-asserted-by":"crossref","unstructured":"C.\u00a0Courcoubetis and M.\u00a0Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857\u2013907, July 1995.","key":"17_CR4","DOI":"10.1145\/210332.210339"},{"unstructured":"L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1998.","key":"17_CR5"},{"unstructured":"P. Dhariwal, Ch. Hesse, O. Klimov, A. Nichol, M. Plappert, A. Radford, J. Schulman, S. Sidor, Y. Wu, and P. Zhokhov. Openai baselines. \nhttps:\/\/github.com\/openai\/baselines\n\n, 2017.","key":"17_CR6"},{"doi-asserted-by":"crossref","unstructured":"D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation relations. In Computer Aided Verification, pages 255\u2013265, July 1991. LNCS 575.","key":"17_CR7","DOI":"10.1007\/3-540-55179-4_25"},{"doi-asserted-by":"crossref","unstructured":"A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In Automated Technology for Verification and Analysis, pages 122\u2013129, 2016.","key":"17_CR8","DOI":"10.1007\/978-3-319-46520-3_8"},{"doi-asserted-by":"crossref","unstructured":"K.\u00a0Etessami, T.\u00a0Wilke, and R.\u00a0A. Schuller. Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput., 34(5):1159\u20131175, 2005.","key":"17_CR9","DOI":"10.1137\/S0097539703420675"},{"doi-asserted-by":"crossref","unstructured":"S.\u00a0Gurumurthy, R.\u00a0Bloem, and F.\u00a0Somenzi. Fair simulation minimization. In Computer Aided Verification (CAV\u201902), pages 610\u2013623, July 2002. LNCS 2404.","key":"17_CR10","DOI":"10.1007\/3-540-45657-0_51"},{"unstructured":"E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang. Lazy probabilistic model checking without determinisation. In Concurrency Theory, pages 354\u2013367, 2015.","key":"17_CR11"},{"doi-asserted-by":"crossref","unstructured":"E.\u00a0M. Hahn, M.\u00a0Perez, S.\u00a0Schewe, F.\u00a0Somenzi, A.\u00a0Trivedi, and D.\u00a0Wojtczak. Omega-regular objectives in model-free reinforcement learning. In Tools and Algorithms for the Construction and Analysis of Systems, pages 395\u2013412, 2019. LNCS 11427.","key":"17_CR12","DOI":"10.1007\/978-3-030-17462-0_27"},{"unstructured":"E. M. Hahn, M. Perez, F. Somenzi, A. Trivedi, S. Schewe, and D. Wojtczak. Good-for-MDPs automata. arXiv e-prints, abs\/1909.05081, September 2019.","key":"17_CR13"},{"doi-asserted-by":"crossref","unstructured":"T.\u00a0Henzinger, O.\u00a0Kupferman, and S.\u00a0Rajamani. Fair simulation. In Concurrency Theory, pages 273\u2013287, 1997. LNCS 1243.","key":"17_CR14","DOI":"10.1007\/3-540-63141-0_19"},{"doi-asserted-by":"crossref","unstructured":"T.\u00a0A. Henzinger and N.\u00a0Piterman. Solving games without determinization. In Computer Science Logic, pages 394\u2013409, September 2006. LNCS 4207.","key":"17_CR15","DOI":"10.1007\/11874683_26"},{"doi-asserted-by":"crossref","unstructured":"D. Kini and M. Viswanathan. Optimal translation of LTL to limit deterministic automata. In Tools and Algorithms for the Construction and Analysis of Systems, pages 113\u2013129, 2017.","key":"17_CR16","DOI":"10.1007\/978-3-662-54580-5_7"},{"doi-asserted-by":"crossref","unstructured":"J. Klein, D. M\u00fcller, Ch. Baier, and S. Kl\u00fcppelholz. Are good-for-games automata good for probabilistic model checking? In Language and Automata Theory and Applications, pages 453\u2013465. Springer, 2014.","key":"17_CR17","DOI":"10.1007\/978-3-319-04921-2_37"},{"doi-asserted-by":"crossref","unstructured":"J. Klein, D. M\u00fcller, Ch. Baier, and S. Kl\u00fcppelholz. Are good-for-games automata good for probabilistic model checking? In Language and Automata Theory and Applications, pages 453\u2013465, 2014.","key":"17_CR18","DOI":"10.1007\/978-3-319-04921-2_37"},{"doi-asserted-by":"crossref","unstructured":"J. K\u0159et\u00ednsk\u00fd, T. Meggendorfer, S. Sickert, and Ch. Ziegler. Rabinizer 4: from LTL to your favourite deterministic automaton. In Computer Aided Verification, pages 567\u2013577. Springer, 2018.","key":"17_CR19","DOI":"10.1007\/978-3-319-96145-3_30"},{"doi-asserted-by":"crossref","unstructured":"J. K\u0159et\u00ednsk\u00fd, T. Meggendorfer, and S. Sickert. Owl: A library for $$\\omega $$-words, automata, and LTL. In Automated Technology for Verification and Analysis, pages 543\u2013550, 2018.","key":"17_CR20","DOI":"10.1007\/978-3-030-01090-4_34"},{"unstructured":"R. Milner. An algebraic definition of simulation between programs. Int. Joint Conf. on Artificial Intelligence, pages 481\u2013489, 1971.","key":"17_CR21"},{"doi-asserted-by":"crossref","unstructured":"N.\u00a0Piterman. From deterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 3(3):1\u201321, 2007.","key":"17_CR22","DOI":"10.2168\/LMCS-3(3:5)2007"},{"doi-asserted-by":"crossref","unstructured":"M.\u00a0L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, New York, NY, USA, 1994.","key":"17_CR23","DOI":"10.1002\/9780470316887"},{"unstructured":"S. Safra. Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, March 1989.","key":"17_CR24"},{"unstructured":"S.\u00a0Schewe. Beyond hyper-minimisation\u2014minimising DBAs and DPAs isNP-complete. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages 400\u2013411, 2010.","key":"17_CR25"},{"doi-asserted-by":"crossref","unstructured":"S. Schewe and T. Varghese. Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In Automated Technology for Verification and Analysis, pages 42\u201356, 2012.","key":"17_CR26","DOI":"10.1007\/978-3-642-33386-6_5"},{"doi-asserted-by":"crossref","unstructured":"S. Schewe and T. Varghese. Determinising parity automata. In Mathematical Foundations of Computer Science, pages 486\u2013498, 2014.","key":"17_CR27","DOI":"10.1007\/978-3-662-44522-8_41"},{"unstructured":"J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov. Proximal policy optimization algorithms. CoRR, abs\/1707.06347, 2017.","key":"17_CR28"},{"doi-asserted-by":"crossref","unstructured":"S.\u00a0Sickert, J.\u00a0Esparza, S.\u00a0Jaax, and J.\u00a0K\u0159et\u00ednsk\u00fd. Limit-deterministic B\u00fcchi automata for linear temporal logic. In Computer Aided Verification, pages 312\u2013332, 2016. LNCS 9780.","key":"17_CR29","DOI":"10.1007\/978-3-319-41540-6_17"},{"doi-asserted-by":"crossref","unstructured":"S. Sickert and J. K\u0159et\u00ednsk\u00fd. MoChiBA: Probabilistic LTL model checking using limit-deterministic B\u00fcchi automata. In Automated Technology for Verification and Analysis, pages 130\u2013137, 2016.","key":"17_CR30","DOI":"10.1007\/978-3-319-46520-3_9"},{"doi-asserted-by":"crossref","unstructured":"F.\u00a0Somenzi and R.\u00a0Bloem. Efficient B\u00fcchi automata from LTL formulae. In Computer Aided Verification, pages 248\u2013263, July 2000. LNCS 1855.","key":"17_CR31","DOI":"10.1007\/10722167_21"},{"doi-asserted-by":"crossref","unstructured":"M.-H. Tsai, S.\u00a0Fogarty, M.\u00a0Y. Vardi, and Y.-K. Tsay. State of B\u00fcchi complementation. Logical Mehods in Computer Science, 10(4), 2014.","key":"17_CR32","DOI":"10.2168\/LMCS-10(4:13)2014"},{"doi-asserted-by":"crossref","unstructured":"M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics. In Computer Aided Verification, pages 883\u2013889, 2013.","key":"17_CR33","DOI":"10.1007\/978-3-642-39799-8_62"},{"doi-asserted-by":"crossref","unstructured":"M. Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Foundations of Computer Science, pages 327\u2013338, 1985.","key":"17_CR34","DOI":"10.1109\/SFCS.1985.12"},{"unstructured":"E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning Figshare (2020), \nhttps:\/\/doi.org\/10.6084\/m9.figshare.11882739\n\n.","key":"17_CR35"},{"unstructured":"A. Hartmanns and M. Seidl. tacas20ae.ova. Figshare (2019) \nhttps:\/\/doi.org\/10.6084\/m9.figshare.9699839.v2","key":"17_CR36"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:12:31Z","timestamp":1597929151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","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":"155","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":"40","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":"8","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":"26% - 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","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":"14","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}