一句话：提出反例引导的参数化无限状态反应式合成方法，可生成可实例化并带不变式/秩函数证明的系统。
论文研究如何合成一个参数化的无限状态反应式系统，使其能针对不同参数取值实例化。规约采用参数化时序逻辑，既包含数据变量，也包含刻画环境性质的参数。方法是一个反例引导的四步循环：先对若干小参数实例用已有技术合成具体系统；再用反合一与语法引导综合将具体系统泛化为参数化程序，并把程序差异表示为参数的函数；随后构造由不变式和秩函数组成的证明候选；最后检查证明候选与程序的一致性。若证明成功，则参数化程序有效；若失败，则找出导致失败的参数值并将其新具体实例加入第一步。作者在新例子和文献中手工参数化的例子上评估了该方法。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MaderbacherB26,
title = {Parameterized Infinite-State Reactive Synthesis},
author = {Benedikt Maderbacher and Roderick Bloem},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776726}
}