通过函数综合实现可预测且高性能的模理论反应式综合
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
AI总结：
该研究提出首个针对LTLt的完整静态反应式综合方法，结合布尔抽象与函数综合生成确定性控制器，兼具可预测性、高效性及输出优化能力。
摘要：
反应式综合是从时序逻辑规约生成正确控制器的过程。经典的LTL反应式综合将（命题）LTL作为规约语言。布尔抽象可将LTLt规约（即命题被来自理论$\textit{calT}$的文字替换的LTL）规约为等可实现性的LTL规约。本文将这些结果扩展为完整的静态综合流程。所综合的系统从环境接收丰富理论$\textit{calT}$中变量的估值，并输出$\textit{calT}$中系统变量的估值。我们使用抽象方法从LTL规约综合出反应式布尔控制器，并将其与函数综合相结合，得到原始LTLt规约的静态控制器。我们还证明该方法支持响应优化：控制器可优化其输出，例如始终提供最小的安全值。这是首个针对LTLt的完整静态综合方法，其生成的是确定性程序，因此具备可预测性与高效性。
英文摘要：
Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
