SynthLearn: A Tool for Guided Reactive Synthesis

In this paper, we introduce the SynthLearn tool. It implements an algorithm for reactive synthesis using LTL specifications, supplemented with examples of desired execution prefixes. Using automata learning techniques and zero-sum two player games, the synthesis procedure produces a Mealy machine that realizes the LTL specification and matches the given examples, whenever possible. By providing desired execution prefixes, users can guide the synthesis towards interesting solutions without having to specify low-level properties in LTL. We demonstrate the tool’s ability to produce effective solutions with a series of examples. Our tool can be accessed through a user-friendly web interface.