Petri Games: A Semantic and Algorithmic Approach for the Efficient Synthesis of Distributed Reactive Systems

Petri Games：分布式反应系统高效综合的语义和算法方法

• 批准号: 392735815
• 负责人: Professor Dr. Bernd Finkbeiner
• 金额: --
• 依托单位: Abteilung Entwicklung korrekter Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/392735815?language=en
• 关键词: Petri; Games; Semantic; Algorithmic; Approach

The reactive synthesis problem considers a specification of a reactive system and asks for an implementation that satisfies the specification for all possible behaviors of the system's environment. A particularly interesting version of the problem, with huge potential for practical applications, is the synthesis of distributed systems, consisting of multiple concurrent processes. However, most results on the synthesis problem for distributed systems are negative. In two well-studied settings, the Pnueli/Rosner model and Zielonka's asynchronous automata, distributed synthesis has extremely high complexity (nonelementary) or is even undecidable. The goal of the proposed project is to develop a new setting for the synthesis of distributed systems where the synthesis problem can be solved with affordable cost, and that is, at the same time, sufficiently powerful to express the synthesis problems of realistic distributed systems.Our proposed setting is based on Petri games, a game-theoretic extension of Petri nets. In previous work, we have shown that synthesis problems for distributed systems from manufacturing and workflow scenarios can be modeled as Petri games. We have also shown that under certain restrictions, the winning strategy of a Petri game, which corresponds to a distributed implementation, can be determined efficiently. The goal of the proposed project is achieved by extending Petri games to a full framework for the synthesis of distributed systems. The proposed work targets both the semantic foundations of Petri games and efficient algorithms for solving Petri games. The new semantic concepts will make Petri games more expressive and more compact, and thus applicable to realistic distributed systems. The new algorithms will generalize the existing algorithms, incorporating, in particular, the new semantic concepts, while maintaining affordable complexity. We will evaluate our approach on two realistic application areas that are out of reach for synthesis today: smart factories and automated access control systems in large buildings.Overall, this project will develop the first practical synthesis approach for distributed systems, including the necessary models, algorithms, and tools. We expect that our synthesis approach will have impact beyond the immediate synthesis community into areas such as semantics, distributed systems design, and autonomous systems.

反应性综合问题考虑反应性系统的规范，并要求实现满足系统环境的所有可能行为的规范。这个问题的一个特别有趣的版本，具有巨大的实际应用潜力，是由多个并发进程组成的分布式系统的合成。然而，对于分布式系统的综合问题，大多数结果都是否定的。在Pnueli/Rosner模型和Zielonka的异步自动机这两个已被充分研究的环境中，分布式综合具有极高的复杂性(非初等)，甚至是不可判定的。该项目的目标是开发一种新的分布式系统综合环境，该环境能够以负担得起的成本解决综合问题，同时足够强大地表达现实分布式系统的综合问题。我们所提出的环境是基于Petri网的博弈论扩展。在以前的工作中，我们已经证明了来自制造和工作流场景的分布式系统的综合问题可以建模为Petri博弈。我们还证明了在一定的约束条件下，可以有效地确定对应于分布式实现的PETRI博弈的获胜策略。该项目的目标是通过将PETRI博弈扩展到一个完整的分布式系统综合框架来实现的。所提出的工作既针对PETRI对策的语义基础，也针对求解PETRI对策的高效算法。新的语义概念将使Petri网游戏更具表现力和紧凑性，从而适用于现实的分布式系统。新的算法将推广现有的算法，特别是合并新的语义概念，同时保持负担得起的复杂性。我们将在两个现实应用领域对我们的方法进行评估：智能工厂和大型建筑中的自动访问控制系统。总的来说，这个项目将开发第一个实用的分布式系统综合方法，包括必要的模型、算法和工具。我们预计，我们的综合方法将产生影响，超越直接综合社区，进入语义、分布式系统设计和自治系统等领域。