Automated Repair of Unrealisable LTL Specifications Guided by Model Counting
This addresses the issue of unrealisable specifications for developers and engineers in formal methods and automated synthesis, though it appears incremental as it builds on existing repair concepts with a new heuristic.
The paper tackles the problem of unrealisable Linear-Time Temporal Logic (LTL) specifications in reactive synthesis by presenting AuRUS, a search-based repair approach that uses syntactic and semantic similarities, including a new heuristic based on model counting; it successfully repaired all tested specifications and showed improved scalability and uniqueness of solutions compared to related techniques.
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.