Symbolically synthesizing small circuits

Reactive synthesis, where a finite-state system is automatically generated from its specification, is a particularly ambitious way to engineer correct-by-construction systems. In this paper, we propose implementation-extraction based on computational learning of Boolean functions as a final synthesis step in order to obtain small and fast circuits for realizable specifications in a symbolic way. Our starting point is a restriction of the system player´s choices in a synthesis game such that all remaining strategies are winning. Such games are used in most symbolic synthesis tools, and hence, our technique is not tied to one specific synthesis workflow, but rather supports a large variety of these. We present several variants of our implementation-learning approach, including one based on Bshouty´s monotone theory. The key idea is the efficient use of the system player´s freedom in the game. Our experimental results show a significant reduction of implementation size compared to previous methods, while maintaining reasonable computation times.