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，尤其是通过反映他们各自的需求。我们的第二个工作包将解决使用完整信息构建控制器的简单问题，而第三个工作包将解决这些技术对控制器的概括，但对于分布式控制器，对于分布式控制器，有关系统状态的等效信息，与离散系统不同，抽象（或限制性观察力）在考虑这些系统不完整的信息时扮演着最重要的角色。事实证明，这种特殊类型的抽象经常简化最佳策略的构建：最佳的抽吸策略（以及其存在的证明）比依赖时间依赖的构建的构建要简单得多。第四个工作套餐指的是这些结果的庞大涉及分配的调度程序，以分配不同的观察力和质量的质量，我们将质量和四个属性。第五工作包我们将重点介绍算法方面，例如模型检查和优化问题的适当数据结构的开发和选择，并开发原型实现，这些实现是为其选择开发方法的适用性的概念证明。这些概念验证实现也将在确定项目中定义的目标实现中开发的技术的适用性和潜力方面发挥重要作用，并作为将我们的结果传播以进行传播和开发目的的方式。