This paper introduces DG-StlRepair, a framework that uses formula decomposition to guide counterexample generation for repairing Signal Temporal Logic specifications. It decomposes STL specifications into sub-formulas, identifies fault locations, and generates targeted counterexamples for precise repairs, addressing limitations in existing CEGIS-based methods.
Key findings
DG-StlRepair leverages hierarchical formula decomposition to guide counterexample generation.
The framework supports multiple repair classes including temporal bound relaxation and predicate adjustment.
A comprehensive validation plan includes benchmarks from autonomous driving and medical device domains.
Limitations & open questions
The framework's scalability to very large STL specifications is yet to be tested.
The approach's effectiveness in diverse real-world applications needs further validation.