We propose a method to synthesize a parameterized infinite-state system that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as parameters that encode properties of the environment. Our synthesis method runs in a counterexample guided loopconsisting of four steps: (1) we synthesize concrete systems for some small parameter instantiations using existing techniques. (2) We generalize the concrete systems into a parameterized program. (3) We create a proof candidate consisting of an invariant and a ranking function. (4) We check the proof candidate for consistency with the program. If the proof succeeds, the parameterized program is valid. Otherwise, we identify a parameter value for which it fails and add a new concrete instance to step one. To generalize programs and create proof candidates, we use a combination of anti-unification and syntax-guided synthesis to express the differences between the programs as a function of the parameters. We evaluate our approach on new examples and examples from the literature that are manually parameterized.

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.