Synthesis from Infinite-State Generalized Reactivity(1) Specifications
摘要
Reactive synthesis is used to automatically generate circuits or programs from temporal logic specifications. In propositional reactive synthesis, generalized reactivity(1) (GR(1)) has proven to be a good compromise between expressiveness and performance. In domains like cyber-physical systems, however, programs must operate on data such as integers or reals, resulting in an infinite state space. This paper shows how to achieve the advantages of GR(1) to infinite-state reactive synthesis. We show how to use an SMT solver to solve the synthesis problem and present techniques to efficiently compute the enforceable predecessor and optimize the fixpoint computation. We show how to generate efficient programs as the result of the synthesis procedure, using techniques that are different from the circuit generation methods used in the propositional domain. We have implemented our method as a prototype to show its efficiency on several existing and new benchmarks.