ITR: Synthesis and Control of Infinite-state Reactive Systems

这项工作的目的是建立一个统一的框架，用于基于时间规范的无限状态反应系统的综合和控制。通过综合，完整的程序直接从其规范生成。通过控制，给出了系统的一部分，任务是生成与给定组件交互的模块，从而使整个系统满足其规范。该框架将包括一个代表无限博弈、控制、可实现性和反应系统综合概念的计算模型，一种可以为系统组件集合分配目标(获胜条件)的规范语言，以及用于解决无限状态情况下各种形式的综合和控制问题的演绎算法方法。该框架的起点将是建立在为有限状态反应系统的算法综合和控制而开发的模型和方法的理论基础上。这些方法将与为反应系统的演绎验证和抽象解释而开发的方法相结合，并与函数程序的演绎综合技术相结合，以允许无限状态系统的综合和控制。对这一方法的初步调查，在这项提案中描述，也被接受发表，是有希望的。

The objective of the proposed work is to develop a unified frameworkfor synthesis and control of infinite-state reactive systems based ontemporal specifications. With synthesis, the full program isgenerated directly from its specification. With control, part of thesystem is given and the task is to generate the modules interactingwith the given components such that the overall system satisfies itsspecification. The framework will include a computational model torepresent the notions of infinite games, control, realizability, andsynthesis of reactive systems, a specification language that canassign goals (winning conditions) to sets of system components, anddeductive-algorithmic methods to solve the synthesis and controlproblems in their various forms for the infinite-state case.The starting point for this framework will be a theoretical foundationbuilt on the models and methods developed for algorithmic synthesisand control of finite-state reactive systems. These methods will becombined with methods developed for deductive verification andabstract interpretation of reactive systems, and with deductivesynthesis techniques for functional programs to allow the synthesisand control of infinite-state systems. Preliminary investigations intothis approach, described in this proposal and also accepted forpublication, are promising.