参数化无限状态反应式综合

《Proceedings of the ACM on Programming Languages》：Parameterized Infinite-State Reactive Synthesis

本文提出了一种参数化无限状态系统的合成方法，通过四步循环：基于现有技术生成具体实例、利用反统合和语法引导合成泛化程序、构建包含不变式和排名函数的证明候选、验证候选与程序的一致性，若失败则迭代更新参数。该方法在自定义和文献案例中验证了有效性。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

我们提出了一种合成参数化无限状态系统的方法，该系统可以为不同的参数值进行实例化。规范采用参数化时态逻辑表示，允许使用数据变量以及编码环境属性的参数。我们的合成方法通过一个由四个步骤组成的反例引导循环来运行：（1）使用现有技术为一些小的参数值实例化合成具体系统；（2）将这些具体系统泛化为参数化程序；（3）创建一个包含不变量和排序函数的证明候选者；（4）检查证明候选者与程序的一致性。如果证明成功，则参数化程序有效；否则，我们确定一个导致失败的参数值，并将该参数值添加到第一步中。为了泛化程序并创建证明候选者，我们结合使用反统一和语法引导的合成方法来表达程序之间的差异作为参数的函数。我们在新的示例以及文献中手动参数化的示例上评估了我们的方法。

人工智能摘要

人工智能生成摘要（实验性）

此摘要是使用自动化工具生成的，不是由文章作者编写或审核的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解本文的工作。它旨在补充作者提供的摘要，后者仍是论文的主要摘要。完整文章是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进和未来重新生成的版本。

要查看此由人工智能生成的通俗语言摘要，您必须具有高级访问权限。