Personal tools
You are here: Home Events Abstract Archives 2006-2007 Safraless Compositional Synthesis

Safraless Compositional Synthesis

Moshe Y. Vardi Rice University 4pm Tuesday 18th April 2006 Room 2511, JCMB, King's Buildings

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.

Document Actions