Verification problems in stochastic games

研究项目的目的是考虑在不一定是有限的图形上玩游戏的问题。这些游戏可以在各种框架中进行，包括但不限于具有不同规格的随机游戏（例如带有计数器的马尔可夫决策过程）。我们将考虑的游戏类型包括平均收益游戏、能量游戏和平价游戏等。这个项目的主要目标是获得关于上述游戏类型的新的或更好的可计算性和复杂性结果。为了获得这些关于游戏规格的结果，我很可能会使用逻辑、代数、自动机理论和数据科学技术。在第4月底之前，我将完成一篇文献综述，并提交一份大纲提案。在第一年结束时，将进行第一年回顾。到第二年结束的时候，我会提交一份进度报告，还有一张海报。在我的第三年，我将在年底提交论文大纲，在研讨会上展示我的工作，并提交论文草稿和进度报告，最后在三年半后提交论文。

The aim of the research project is to consider questions concerning games played on graphs which are not necessarily finite. These games can be played in a variety of frameworks including, but not limited to stochastic games with different kinds of specifications (eg Markov Decision Process with a counter). Types of games that will be considered will include mean payoff games, energy games and parity games amongst others.The main objective of this project is to derive new or finer computability and complexity results concerning the aforementioned types of games. To derive these results about game specifications I will most likely employ logical, algebraic, automata theoretic and data scientific techniques.By the end of month 4, I will produce a literature review and submit an outline proposal. At the end of the first year a First Year Review will take place. By the end of the second year I will have submitted a progress report as well as optionally a poster. During my third year I will submit a thesis outline, present my work at a seminar as well as submit a draft thesis and progress report by the end of the year, before finally submitting my thesis after three and a half years.