Facets of Synthesis: Revisiting Church's Problem

10 years 4 months ago
Facets of Synthesis: Revisiting Church's Problem
In this essay we discuss the origin, central results, and some perspectives of algorithmic synthesis of nonterminating reactive programs. We recall the fundamental questions raised more than 50 years ago in “Church’s Synthesis Problem” that led to the foundation of the algorithmic theory of infinite games. We outline the methodology developed in more recent years for solving such games and address related automata theoretic problems that are still unresolved. 1 Prologue The objective of “synthesis” is to pass from a specification to a program realizing it. This is a central task in computer science, and – unfortunately or fortunately, depending on the point of view – its solution cannot in general be automatized. However, there are classes of specifications for which algorithmic synthesis is possible. In the present paper we deal with a fundamental class of this kind, the regular specifications for nonterminating reactive programs. In another terminology, this amounts...
Wolfgang Thomas
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Authors Wolfgang Thomas
Comments (0)