322
E. M. Hahn et al.
References
1. T. Babiak, M. Kˇ ret´ ınsk´ y, V. Reh´ ak, and J. Strejcek. LTL to B¨ uchi automata translation:
Fast and more deterministic. In Tools and Algorithms for the Construction and Analysis of
Systems, pages 95–109, 2012.
2. Ch. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
3. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Foundations of Computer Science, pages 338–345. IEEE, 1988.
4. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM,
42(4):857–907, July 1995.
5. L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University,
1998.
6. P. Dhariwal, Ch. Hesse, O. Klimov, A. Nichol, M. Plappert, A. Radford, J. Schulman,
S. Sidor, Y. Wu, and P. Zhokhov. Openai baselines. https://github.com/openai/baselines,
2017.
7. D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation
relations. In Computer Aided Verification, pages 255–265, July 1991. LNCS 575.
8. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 - A
framework for LTL and ω-automata manipulation. In Automated Technology for Verification
and Analysis, pages 122–129, 2016.
9. K. Etessami, T. Wilke, and R. A. Schuller. Fair simulation relations, parity games, and state
space reduction for B¨ uchi automata. SIAM J. Comput., 34(5):1159–1175, 2005.
10. S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In Computer
Aided Verification (CAV’02), pages 610–623, July 2002. LNCS 2404.
11. E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang. Lazy probabilistic model checking
without determinisation. In Concurrency Theory, pages 354–367, 2015.
12. E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak. Omega-regular
objectives in model-free reinforcement learning. In Tools and Algorithms for the Construction and Analysis of Systems, pages 395–412, 2019. LNCS 11427.
13. 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.
14. T. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Concurrency Theory,
pages 273–287, 1997. LNCS 1243.
15. T. A. Henzinger and N. Piterman. Solving games without determinization. In Computer
Science Logic, pages 394–409, September 2006. LNCS 4207.
16. 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–129, 2017.
17. J. Klein, D. M¨ uller, Ch. Baier, and S. Kl¨ uppelholz. Are good-for-games automata good for
probabilistic model checking? In Language and Automata Theory and Applications, pages
453–465. Springer, 2014.
18. J. Klein, D. M¨ uller, Ch. Baier, and S. Kl¨ uppelholz. Are good-for-games automata good for
probabilistic model checking? In Language and Automata Theory and Applications, pages
453–465, 2014.
19. J. Kˇ ret´ ınsk´ y, T. Meggendorfer, S. Sickert, and Ch. Ziegler. Rabinizer 4: from LTL to your
favourite deterministic automaton. In Computer Aided Verification, pages 567–577. Springer,
2018.
20. J. Kˇ ret´ ınsk´ y, T. Meggendorfer, and S. Sickert. Owl: A library for ω-words, automata, and
LTL. In Automated Technology for Verification and Analysis, pages 543–550, 2018.
21. R. Milner. An algebraic definition of simulation between programs. Int. Joint Conf. on
Artificial Intelligence, pages 481–489, 1971.
E. M. Hahn et al.
References
1. T. Babiak, M. Kˇ ret´ ınsk´ y, V. Reh´ ak, and J. Strejcek. LTL to B¨ uchi automata translation:
Fast and more deterministic. In Tools and Algorithms for the Construction and Analysis of
Systems, pages 95–109, 2012.
2. Ch. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
3. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Foundations of Computer Science, pages 338–345. IEEE, 1988.
4. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM,
42(4):857–907, July 1995.
5. L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University,
1998.
6. P. Dhariwal, Ch. Hesse, O. Klimov, A. Nichol, M. Plappert, A. Radford, J. Schulman,
S. Sidor, Y. Wu, and P. Zhokhov. Openai baselines. https://github.com/openai/baselines,
2017.
7. D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation
relations. In Computer Aided Verification, pages 255–265, July 1991. LNCS 575.
8. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 - A
framework for LTL and ω-automata manipulation. In Automated Technology for Verification
and Analysis, pages 122–129, 2016.
9. K. Etessami, T. Wilke, and R. A. Schuller. Fair simulation relations, parity games, and state
space reduction for B¨ uchi automata. SIAM J. Comput., 34(5):1159–1175, 2005.
10. S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In Computer
Aided Verification (CAV’02), pages 610–623, July 2002. LNCS 2404.
11. E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang. Lazy probabilistic model checking
without determinisation. In Concurrency Theory, pages 354–367, 2015.
12. E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak. Omega-regular
objectives in model-free reinforcement learning. In Tools and Algorithms for the Construction and Analysis of Systems, pages 395–412, 2019. LNCS 11427.
13. 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.
14. T. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Concurrency Theory,
pages 273–287, 1997. LNCS 1243.
15. T. A. Henzinger and N. Piterman. Solving games without determinization. In Computer
Science Logic, pages 394–409, September 2006. LNCS 4207.
16. 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–129, 2017.
17. J. Klein, D. M¨ uller, Ch. Baier, and S. Kl¨ uppelholz. Are good-for-games automata good for
probabilistic model checking? In Language and Automata Theory and Applications, pages
453–465. Springer, 2014.
18. J. Klein, D. M¨ uller, Ch. Baier, and S. Kl¨ uppelholz. Are good-for-games automata good for
probabilistic model checking? In Language and Automata Theory and Applications, pages
453–465, 2014.
19. J. Kˇ ret´ ınsk´ y, T. Meggendorfer, S. Sickert, and Ch. Ziegler. Rabinizer 4: from LTL to your
favourite deterministic automaton. In Computer Aided Verification, pages 567–577. Springer,
2018.
20. J. Kˇ ret´ ınsk´ y, T. Meggendorfer, and S. Sickert. Owl: A library for ω-words, automata, and
LTL. In Automated Technology for Verification and Analysis, pages 543–550, 2018.
21. R. Milner. An algebraic definition of simulation between programs. Int. Joint Conf. on
Artificial Intelligence, pages 481–489, 1971.