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.