The reactive synthesis problem consists of automatically producing correct-by-construction operational models of systems from high-level formal specifications of their behaviours. However, specifications are often unrealisable, meaning that no system can be synthesised from the specification. To deal with this problem, we present AuRUS, a search-based approach to repair unrealisable Linear-Time Temporal Logic (LTL) specifications. AuRUS aims at generating solutions that are similar to the original specifications by using the notions of syntactic and semantic similarities. Intuitively, the syntactic similarity measures the text similarity between the specifications, while the semantic similarity measures the number of behaviours preserved/removed by the candidate repair. We propose a new heuristic based on model counting to approximate semantic similarity. We empirically assess AuRUS on many unrealisable specifications taken from different benchmarks and show that it can successfully repair all of them. Also, compared to related techniques, AuRUS can produce many unique solutions while showing more scalability.

翻译：反应式合成的问题在于从系统的高级形式化规范中自动产生符合要求的运行模型。然而，规范通常是无法实现的，这意味着无法从规范中合成出系统。针对这个问题，我们提出了AuRUS，一种基于搜索的方法来修复无法实现的线性时态逻辑（LTL）规范。AuRUS旨在通过使用语法和语义相似性的概念来生成与原始规范类似的解决方案。直观地说，语法相似性衡量规范之间的文本相似性，而语义相似性衡量候选修复所保留/删除的行为数量。我们提出了一种基于模型计数的启发式算法来近似语义相似性。我们从不同的基准测试中获取许多无法实现的规范，并对AuRUS进行实证评估，结果表明它可以成功修复所有规范。与相关技术相比，AuRUS可以产生许多独特的解决方案，并且展现了更高的可扩展性。