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).

翻译：反应式综合是指从时序逻辑规约生成正确控制器的过程。经典的LTL反应式综合将（命题）LTL作为规约语言处理。布尔抽象方法允许将LTLt规约（即命题被理论calT中的文字替换的LTL）约化为等可实现性的LTL规约。本文将这些结果扩展为完整的静态综合流程。所综合的系统接收来自环境的、基于丰富理论calT的变量赋值，并输出基于calT的系统变量赋值。我们使用抽象方法从LTL规约综合出反应式布尔控制器，并将其与函数式综合相结合，从而为原始LTLt规约获得静态控制器。我们还证明，该方法支持响应式优化，即控制器能够优化其输出，例如始终提供最小的安全值。这是首个针对LTLt的完整静态综合方法，所生成的控制器为确定性程序（因而具备可预测性与高效性）。