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

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

该研究提出一种参数化无限状态系统合成方法，通过反统合和语法引导合成技术，在四步循环验证中实现系统的一般化。具体包括：针对特定参数生成实例系统、进行参数化程序泛化、构建包含不变式和排名函数的证明候选，最终通过验证循环确保系统在参数变化下的有效性。实验表明该方法能有效处理参数化时态逻辑约束的新旧案例。

　　

摘要AI摘要

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

了解更多登录

摘要

摘要

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

AI摘要

AI生成的摘要（实验性）

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

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的版本。

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