Title: Reactive Synthesis Modulo Theories Using Abstraction Refinement Show Chinese title

Title: 基于抽象精化的理论模数反应综合

Abstract: Reactive synthesis builds a system from a specification given as a temporal logic formula. Traditionally, reactive synthesis is defined for systems with Boolean input and output variables. Recently, new theories and techniques have been proposed to extend reactive synthesis to data domains, which are required for more sophisticated programs. In particular, Temporal stream logic(TSL) (Finkbeiner et al. 2019) extends LTL with state variables, updates, and uninterpreted functions and was created for use in synthesis. We present a synthesis procedure for TSL(T), an extension of TSL with theories. Synthesis is performed using a counter-example guided synthesis loop and an LTL synthesis procedure. Our method translates TSL(T) specifications to LTL and extracts a system if synthesis is successful. Otherwise, it analyzes the counterstrategy for inconsistencies with the theory. If the counterstrategy is theory-consistent, it proves that the specification is unrealizable. Otherwise, we add temporal assumptions and Boolean predicates to the TSL(T) specification and start the next iteration of the the loop. We show that the synthesis problem for TSL (T) is undecidable. Nevertheless our method can successfully synthesize or show unrealizability of several non-Boolean examples. Show Chinese abstract

Abstract: 反应合成从作为时态逻辑公式的规范构建系统。 传统上，反应合成是针对具有布尔输入和输出变量的系统定义的。 最近，提出了新的理论和技术，以将反应合成扩展到数据域，这在更复杂的程序中是必需的。 特别是时态流逻辑（TSL） （Finkbeiner 等人 2019）将 LTL 扩展为包含状态变量、更新和未解释函数，并专为合成而设计。 我们提出了一个 TSL(T) 的合成过程，它是带有理论的 TSL 的扩展。 合成是通过一个反例引导的合成循环和一个 LTL 合成过程来完成的。 我们的方法将 TSL(T) 规范转换为 LTL，并在合成成功时提取一个系统。 否则，它会分析反策略与理论的不一致之处。 如果反策略与理论一致，它将证明规范不可实现。 否则，我们向 TSL(T) 规范中添加时间假设和布尔谓词，并开始循环的下一次迭代。 我们表明 TSL (T) 的合成问题是不可判定的。 尽管如此，我们的方法可以成功合成或证明几个非布尔示例的不可实现性。