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 specification. 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/96/1567/CS-TR-96-1567.pdf