Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

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 a search-based approach to repair unrealisable specifications (expressed in LTL). Our approach aims at generating similar solutions to the original specifications. To deal with this, we introduce the concept of syntactic and semantic similarity. Intuitively, the syntactic similarity measures how syntactically similar the specifications are, while the semantic similarity measures the number of behaviours preserved/removed by the candidate repair. To approximate semantic similarity, we propose a new heuristic based on model counting. We empirically assess our approach on 26 case studies taken from different benchmarks, and show that it can fix all unrealisable specifications. Moreover, compared to related techniques, our approach is able to produce hundreds of unique solutions while applying to a larger class of LTL formulas.