Synthesis and Verification in Markov Game Structures

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

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.