Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

TL;DR

AuRUS is a novel search-based method that repairs unrealisable LTL specifications by leveraging model counting to preserve behaviors, demonstrating high success and scalability across diverse benchmarks.

Contribution

Introduces AuRUS, a new heuristic approach for repairing unrealisable LTL specifications using model counting to measure semantic similarity.

Findings

Successfully repaired all tested unrealisable specifications.

Produces many unique solutions compared to existing techniques.

Shows superior scalability in empirical evaluations.

Abstract

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.