基于模型计数的不可实现 LTL 规范自动修复
软件工程
2023-04-17 v2
摘要
反应式合成问题旨在从系统行为的高层形式化规范中自动生成构造即正确的系统操作模型。然而，规范常常是不可实现的，即无法从该规范合成出任何系统。为应对此问题，我们提出 AuRUS，一种基于搜索的方法来修复不可实现的线性时序逻辑（Linear-Time Temporal Logic, LTL）规范。AuRUS 旨在利用语法相似性和语义相似性的概念，生成与原始规范相似的解决方案。直观而言，语法相似性衡量规范间的文本相似度，而语义相似性衡量候选修复所保留或移除的行为数量。我们提出了一种基于模型计数的新启发式方法来近似语义相似性。我们在取自不同基准测试的许多不可实现规范上对 AuRUS 进行了实证评估，结果表明它可成功修复所有这些规范。此外，与相关技术相比，AuRUS 能生成许多独特的解决方案，同时表现出更好的可扩展性。
引用
@article{arxiv.2105.12595,
title = {Automated Repair of Unrealisable LTL Specifications Guided by Model Counting},
author = {Matías Brizzio and Maxime Cordy and Mike Papadakis and César Sánchez and Nazareno Aguirre and Renzo Degiovanni},
journal= {arXiv preprint arXiv:2105.12595},
year = {2023}
}