Games for Analysis and Synthesis of Interactive Computational Systems (GASICS)

交互式计算系统分析与综合游戏 (GASICS)

• 批准号: 72093553
• 负责人: Professor Dr. Wolfgang Thomas
• 金额: --
• 依托单位: Informatik 7 - Lehrstuhl Logik und Theorie diskreter Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2008
• 资助国家: 德国
• 起止时间: 2007-12-31 至 2011-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/72093553?language=en
• 关键词: Games; Analysis; Synthesis; Interactive; Computational

Our approach is to generalize transition systems and automata – models of computation of the classical approach to verification – by the more flexible (and mathematically deeper) game-theoretic framework. There are initial results in this area, and our aim is to advance them towards a usable framework and methodology in the verification and design of complex systems. Our objectives are complementary to fields like game theoretic semantics in logic and the theory of programming. With the proposed approach, we also aim to contribute to a convergence of our community with the important community of control theory that deals with the behavior of dynamical systems.Objectives and motivations - Our long term objective is the definition of a modern systems theory where systems are modeled as interacting processes that are potential collaborators or adversaries, and where important aspects like communication, timing information, data, probability, etc. can be adequately modeled.As computer systems are deployed more and more in safety critical environments, there is a need for a methodology to design, synthesize and formally verify complex interacting computational systems. This modern systems theory should help the designers to model complex computer based systems in a rigorous way and allow them to reason formally about their correctness. Our research should contribute substantially to the creation of such a methodology.

我们的方法是通过更灵活（数学上更深入）的博弈论框架来推广转换系统和自动机——经典验证方法的计算模型。在这个领域有初步的结果，我们的目标是在复杂系统的验证和设计中，将它们推进到一个可用的框架和方法。我们的目标是补充领域，如博弈论语义在逻辑和规划理论。通过提出的方法，我们还旨在促进我们的社区与处理动态系统行为的重要控制理论社区的收敛。目标和动机-我们的长期目标是现代系统理论的定义，其中系统被建模为交互过程，这些过程是潜在的合作者或对手，并且像通信，定时信息，数据，概率等重要方面可以充分建模。随着计算机系统越来越多地部署在安全关键环境中，需要一种方法来设计、综合和正式验证复杂的交互计算系统。这种现代系统理论应该帮助设计者以严格的方式对复杂的基于计算机的系统进行建模，并允许他们对其正确性进行正式的推理。我们的研究应该对创建这样一种方法作出重大贡献。