Abstract
Reactive synthesis is the process of generating correct controllers fromtemporal logic specifications. Classical LTL reactive synthesis handles(propositional) LTL as a specification language. Boolean abstractions allowreducing LTLt specifications (i.e., LTL with propositions replaced by literalsfrom a theory calT), into equi-realizable LTL specifications. In this paper weextend these results into a full static synthesis procedure. The synthesizedsystem receives from the environment valuations of variables from a rich theorycalT and outputs valuations of system variables from calT. We use theabstraction method to synthesize a reactive Boolean controller from the LTLspecification, and we combine it with functional synthesis to obtain a staticcontroller for the original LTLt specification. We also show that our methodallows responses in the sense that the controller can optimize its outputs inorder to e.g., always provide the smallest safe values. This is the first fullstatic synthesis method for LTLt, which is a deterministic program (hencepredictable and efficient).