Reactive synthesis is the process of using temporal logic specifications in LTL to generate correct controllers, but its use has been restricted to Boolean specifications. Recently, a Boolean abstraction technique allows to translate LTL T specifications that contain literals in theories into equi-realizable LTL specifications. However, no synthesis procedure exists yet. In synthesis modulo theories, the system to synthesize receives valuations of environment variables in a first-order theory T and outputs valuations of system variables from T . In this paper, we address how to syntheize a full controller using a combination of the static Boolean controller obtained from the Booleanized LTL specification together with dynamic queries to a solver that produces models of a satisfiable existential formulae from T . This is the first method that realizes reactive synthesis modulo theories.

翻译：反应式合成是利用LTL中的时序逻辑规范生成正确控制器的过程，但其应用一直局限于布尔型规范。最近，一种布尔抽象技术允许将包含理论中字词的LTL T规范转化为等可实现性的LTL规范。然而，目前尚不存在相应的合成程序。在模理论合成中，待合成的系统接收一阶理论T中环境变量的取值，并输出T中系统变量的取值。本文探讨如何结合布尔化LTL规范得到的静态布尔控制器与对求解器（该求解器可生成T中可满足存在公式的模型）的动态查询，来合成完整控制器。这是首个实现模理论反应式合成的方法。