Parameterized Infinite-State Reactive Synthesis

TL;DR

This paper introduces a novel synthesis approach for parameterized infinite-state reactive systems using a counterexample-guided loop, combining anti-unification and syntax-guided synthesis to handle data and parameter variables.

Contribution

It presents a new method for synthesizing parameterized systems with a counterexample-guided loop, generalizing concrete systems into parameterized programs with proof validation.

Findings

Successfully applied to literature examples with parameters

Handles data variables and environment properties

Effective in synthesizing parameterized reactive systems

Abstract

We propose a method to synthesize a parameterized infinite-state systems 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 parameter variables that encode properties of the environment. Our synthesis method runs in a counterexample-guided loop consisting of four main steps: First, we use existing techniques to synthesize concrete systems for some small parameter instantiations. Second, we generalize the concrete systems into a parameterized program. Third, we create a proof candidate consisting of an invariant and a ranking function. Fourth, 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 the proof 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 syntactic differences between programs as functions of the parameters. We evaluate our approach on examples from the literature that have been extended with parameters as well as new problems.