Safraless Compositional Synthesis

In automated synthesis, we transform a specification into a system
that is guaranteed to satisfy the specification. In spite of the rich
theory developed for system synthesis, little of this theory has been
reduced to practice. This is in contrast with model-checking
theory, which has led to industrial development and use of formal
verification tools.  We see two main reasons for the lack of practical
impact of synthesis.  The first is algorithmic: synthesis involves
determinization of automata on infinite words, and a solution
of parity games with highly complex state spaces; both problems have
been notoriously resistant to efficient implementation. The second is
methodological: current theory of synthesis assumes a single
comprehensive specification. In practice, however, the specification
is composed of a set of properties, which is typically evolving --
properties may be added, deleted, or modified.

In this work we address both issues. We extend the Safraless synthesis
algorithm of Kupferman and Vardi so that it handles LTL formulas by
translating them to nondeterministic generalized B\"uchi automata.
This leads to an exponential improvement in the complexity of the
algorithm. Technically, our algorithm reduces the synthesis problem to
the emptiness problem of a nondeterministic B\"uchi tree automaton
$\A$.  The generation of $\A$ avoids determinization, avoids the
parity acceptance condition, and is based on an analysis of runs of
universal generalized co-B\"uchi tree automata. The clean and simple
structure of $\A$ enables optimizations and a symbolic
implementation. In addition, it makes it possible to use information
gathered during the synthesis process of properties in the process of
synthesizing their conjunction.