Synthesis and Verification in Markov Game Structures

马尔可夫博弈结构的综合与验证

• 批准号: EP/H046623/1
• 负责人: Sven Schewe
• 金额: $ 42.75万
• 依托单位: University of Liverpool
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FH046623%2F1
• 关键词: Synthesis; Verification; Markov; Game; Structures

To meet the objectives of our project, we will divide our research into five work packages.The first work package is devoted to representing the control problems that we want to approach and to identify benchmarks and case studies as guidelines for relevant demands and measures of success for the applied aspects of our project. The starting point for our models will be- a generalisation of interactive Markov chains to 2.5 player games, a model in which the decisions of the different players are physically separated by assigning them to different states, and- a generalisation of Markov decision processes to Markov games, a model in which the decisions of both (or, more generally, of all) players are entangled and represented in the same node.We will extend these models by representations of the observational and computational power of the controllers under consideration, and formalisations of the--simple--objectives we want to meet.Additionally, we will develop benchmarks and case studies to guide the applied aspects of our project, and to root it in different communities--in particular in engineering and IT--by reflecting their respective demands.Work packages two, three, and four from the theoretic core of our work. Our second work package will address the simple question of constructing controllers with complete information, while a third work package will address the generalisation of these techniques to controllers with incomplete information but, for distributed controllers, equivalent information about the system state.Different to discrete systems, the abstraction (or restricted observability) of time plays a paramount role when considering incomplete information of these systems. This particular type of abstraction has proven to often simplify the construction of optimal strategies: The construction of optimal time-abstract strategies (and the proof of their existence) is much simpler than the construction of time dependent ones.The fourth work package refers to the extension of these results to distributed schedulers with different observational power.For work packages two, three, and four, we will study the decidability of quantitative and qualitative safety and reachability properties.In a fifth work package we will focus on algorithmic aspects like the development and selection of appropriate data structures of the model checking and optimisation problems, and develop prototype implementations that solve as a proof-of-concept for their applicability for a selection of the developed approaches. These proof-of-concept implementations will also play an important role in determining the applicability and potential of the techniques developed in the project on the target implementations defined in the first work package, and as means to communicate our results for dissemination and exploitation purposes.

为了达到我们项目的目标，我们将把我们的研究分为五个工作包。第一个工作包致力于表示我们想要处理的控制问题，并确定基准和案例研究，作为我们项目应用方面的相关需求和成功度量的指导方针。我们模型的起点将是-将交互马尔可夫链概括为2.5人博弈，其中不同参与者的决策通过分配到不同的状态而在物理上分离的模型，以及-将马尔可夫决策过程概括为马尔可夫博弈，其中两个（或更一般地说，所有）参与者的决策纠缠在一起并在同一节点中表示的模型。我们将通过考虑中的控制器的观测和计算能力的表示以及我们想要满足的简单目标的形式化来扩展这些模型。此外，我们将开发基准和案例研究来指导我们项目的应用方面，并通过反映他们各自的需求将其扎根于不同的社区——特别是工程和it领域。工作包二、三、四是我们工作的理论核心。我们的第二个工作包将解决构造具有完整信息的控制器的简单问题，而第三个工作包将解决将这些技术推广到具有不完整信息的控制器，但对于分布式控制器，关于系统状态的等效信息。与离散系统不同的是，当考虑这些系统的不完全信息时，时间的抽象性（或受限的可观测性）起着至关重要的作用。这种特殊类型的抽象被证明经常简化最优策略的构建：最优时间抽象策略的构建（以及它们存在的证明）比时间依赖策略的构建要简单得多。第四个工作包是将这些结果扩展到具有不同观测能力的分布式调度程序。对于工作包2、3和4，我们将研究定量和定性的安全性和可达性属性的可判定性。在第五个工作包中，我们将专注于算法方面，如模型检查和优化问题的适当数据结构的开发和选择，并开发原型实现，以解决其对所开发方法的选择适用性的概念验证。这些概念验证实现也将在确定项目中开发的技术在第一个工作包中定义的目标实现上的适用性和潜力方面发挥重要作用，并作为为了传播和开发目的而交流我们的结果的手段。

项目成果

Finding Approximate Nash Equilibria of Bimatrix Games via Payoff Queries

通过支付查询找到 Bimatrix 博弈的近似纳什均衡

• DOI: 10.1145/2956579
• 发表时间: 2016
• 期刊: ACM Transactions on Economics and Computation
• 影响因子: 1.2
• 作者: Fearnley J

Reachability in two-clock timed automata is PSPACE-complete

• DOI: 10.1016/j.ic.2014.12.004
• 发表时间: 2013-02
• 作者: John Fearnley;M. Jurdzinski

CTL* synthesis via LTL synthesis

通过 LTL 合成进行 CTL* 合成

• DOI: 10.4204/eptcs.260.4
• 发表时间: 2017
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: Bloem R

Approximate Well-supported Nash Equilibria Below Two-thirds

有充分支持的纳什均衡近似低于三分之二

• DOI: 10.1007/s00453-015-0029-3
• 发表时间: 2015
• 期刊: Algorithmica
• 影响因子: 1.1
• 作者: Fearnley J

An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space

• DOI: 10.1007/s10009-019-00509-3
• 发表时间: 2019-06-01
• 期刊: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
• 影响因子: 1.5
• 作者: Fearnley, John;Jain, Sanjay;Wojtczak, Dominik
• 通讯作者: Wojtczak, Dominik