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

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Orna Kupferman, Nir Piterman, Moshe Y. Vardi
• Keywords: CAV 2006, Hardware, Safraless Synthesis Algorithm, Single Comprehensive Specification, Synthesis Involves Determinization