Report Number: CS-TR-96-1567
Institution: Stanford University, Department of Computer Science
Title: Synthesis of Reactive Programs
Author: Anuchitanukul, Anuchit
Date: April 1996
Abstract: We study various problems of synthesizing reactive programs.
A reactive program is a program whose behaviors are not
merely functional relationships between inputs and outputs,
but sequences of actions as well as interactions between the
program and its environment. The goal of program synthesis in
general is to find an implementation of a program such that
the behaviors of the implementation satisfy a given
The reactive behaviors that we study are omega-regular
infinite sequences and regular finite sequences. The domain
of the implementation is (finite) transition systems for
closed system synthesis, and transition system modules for
open system synthesis. We consider various solutions, e.g.
basic, maximal, modular and exact, for any particular
subclasses of the implementation language and investigate how
characteristics of the program such as fairness, number of
processes and composition operations, affect the synthesis
algorithm. In addition to the automata-theoretic algorithms,
we give a synthesis algorithm which synthesizes a program
directly from the linear-time temporal logic ETL.