Starting in the early 80's, a number of algorithmic techniques have been proposed for synthesizing the synchronization kernel of reactive systems from high-level temporal logic specifications. These techniques are based on nontrivial results in logic and automata theory and appear to be quite powerful. Nevertheless, essentially none of this work has found its way to practical use. This talk reviews the main results from this area and tries to identify the main reasons that explain their nonexploitation.
Back to LOPSTR'98 home page