19.4.06
Talk: Safraless Compositional Synthesis
Moshe Y. Vardi. 4pm Tuesday 18th April 2006.
[Phil's comment: Great talk! Vardi went through the formalism step by step, which made it possible for someone like me to follow along and get some understanding of the landscape and the results.]
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.
[Phil's comment: Great talk! Vardi went through the formalism step by step, which made it possible for someone like me to follow along and get some understanding of the landscape and the results.]
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.
