Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

Matías Brizzio, Maxime Cordy, Mike Papadakis +3

The reactive synthesis problem consists of automatically producing correct-by-construction operational models of systems from high-level formal specifications of their behaviours.…