Abstract
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 of 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
Safra's 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 a Safraless synthesis
algorithm, which avoids both Safra's determinization and parity-game
solving. Technically, our algorithm reduces the synthesis problem to
the emptiness problem of a nondeterministic Buechi tree automaton A.
The generation of A avoids determinization, avoids the
parity acceptance condition, and is based on an analysis of runs of
universal co-Buechi 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, enabling compositional synthesis.
Joint work with Orna Kupferman and Nir Piterman.