Reactive synthesis promises the automatic construction of systems that are "correct-by-design." However, the gap between abstract Linear Temporal Logic (LTL) specifications and practical, efficient implementations remains a significant hurdle.
We address the limitations of automatic LTL synthesis by introducing “LTL synthesis with hints” — a novel variant of the LTL synthesis problem that incorporates user guidance in the form of traces to steer synthesis algorithms toward more practical and efficient solutions. By generalizing the user-provided example traces, our approach combines passive learning techniques with existing LTL synthesis algorithms to bridge the gap between abstract specifications and real-world implementations, as demonstrated through a toy-implementation and a series of case studies.