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能生成许多唯一解，同时展现出更高的可扩展性。