Good-for-MDPs Automata
323
22. N. Piterman. From deterministic B¨ uchi and Streett automata to deterministic parity automata.
Logical Methods in Computer Science, 3(3):1–21, 2007.
23. M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming.
John Wiley & Sons, New York, NY, USA, 1994.
24. S. Safra. Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute
of Science, March 1989.
25. S. Schewe. Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete.
In Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages
400–411, 2010.
26. S. Schewe and T. Varghese. Tight bounds for the determinisation and complementation of
generalised B¨ uchi automata. In Automated Technology for Verification and Analysis, pages
42–56, 2012.
27. S. Schewe and T. Varghese. Determinising parity automata. In Mathematical Foundations
of Computer Science, pages 486–498, 2014.
28. J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov. Proximal policy optimization algorithms. CoRR, abs/1707.06347, 2017.
29. S. Sickert, J. Esparza, S. Jaax, and J. Kˇ ret´ ınsk´ y. Limit-deterministic B¨ uchi automata for
linear temporal logic. In Computer Aided Verification, pages 312–332, 2016. LNCS 9780.
30. S. Sickert and J. Kˇ ret´ ınsk´ y. MoChiBA: Probabilistic LTL model checking using limitdeterministic B¨ uchi automata. In Automated Technology for Verification and Analysis, pages
130–137, 2016.
31. F. Somenzi and R. Bloem. Efficient B¨ uchi automata from LTL formulae. In Computer Aided
Verification, pages 248–263, July 2000. LNCS 1855.
32. M.-H. Tsai, S. Fogarty, M. Y. Vardi, and Y.-K. Tsay. State of B¨ uchi complementation. Logical Mehods in Computer Science, 10(4), 2014.
33. M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics.
In Computer Aided Verification, pages 883–889, 2013.
34. M. Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In
Foundations of Computer Science, pages 327–338, 1985.
35. 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),
https://doi.org/10.6084/m9.figshare.11882739
36. A. Hartmanns and M. Seidl. tacas20ae.ova. Figshare (2019)
https://doi.org/10.6084/m9.figshare.9699839.v2
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide a link to the Creative
Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative
Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain
permission directly from the copyright holder.
323
22. N. Piterman. From deterministic B¨ uchi and Streett automata to deterministic parity automata.
Logical Methods in Computer Science, 3(3):1–21, 2007.
23. M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming.
John Wiley & Sons, New York, NY, USA, 1994.
24. S. Safra. Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute
of Science, March 1989.
25. S. Schewe. Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete.
In Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages
400–411, 2010.
26. S. Schewe and T. Varghese. Tight bounds for the determinisation and complementation of
generalised B¨ uchi automata. In Automated Technology for Verification and Analysis, pages
42–56, 2012.
27. S. Schewe and T. Varghese. Determinising parity automata. In Mathematical Foundations
of Computer Science, pages 486–498, 2014.
28. J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov. Proximal policy optimization algorithms. CoRR, abs/1707.06347, 2017.
29. S. Sickert, J. Esparza, S. Jaax, and J. Kˇ ret´ ınsk´ y. Limit-deterministic B¨ uchi automata for
linear temporal logic. In Computer Aided Verification, pages 312–332, 2016. LNCS 9780.
30. S. Sickert and J. Kˇ ret´ ınsk´ y. MoChiBA: Probabilistic LTL model checking using limitdeterministic B¨ uchi automata. In Automated Technology for Verification and Analysis, pages
130–137, 2016.
31. F. Somenzi and R. Bloem. Efficient B¨ uchi automata from LTL formulae. In Computer Aided
Verification, pages 248–263, July 2000. LNCS 1855.
32. M.-H. Tsai, S. Fogarty, M. Y. Vardi, and Y.-K. Tsay. State of B¨ uchi complementation. Logical Mehods in Computer Science, 10(4), 2014.
33. M.-H. Tsai, Y.-K. Tsay, and Y.-S. Hwang. GOAL for games, omega-automata, and logics.
In Computer Aided Verification, pages 883–889, 2013.
34. M. Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In
Foundations of Computer Science, pages 327–338, 1985.
35. 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),
https://doi.org/10.6084/m9.figshare.11882739
36. A. Hartmanns and M. Seidl. tacas20ae.ova. Figshare (2019)
https://doi.org/10.6084/m9.figshare.9699839.v2
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide a link to the Creative
Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative
Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain
permission directly from the copyright holder.