Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical $\mathit{LTL}$ reactive synthesis handles (propositional) $\mathit{LTL}$ as a specification language. Boolean abstractions allow reducing $LT{L}^{\mathcal{T}}$ specifications (i.e., $\mathit{LTL}$ with propositions replaced by literals from a theory $\mathcal{T}$), into equi-realizable $\mathit{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 $\mathcal{T}$ and outputs valuations of system variables from $\mathcal{T}$. We use the abstraction method to synthesize a reactive Boolean controller from the $\mathit{LTL}$ specification, and we combine it with functional synthesis to obtain a static controller for the original $LT{L}^{\mathcal{T}}$ specification. We also show that our method allows adaptive 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 $LT{L}^{\mathcal{T}}$, which is a deterministic program (hence predictable and efficient).