Synthesis of reactive programs
Anuchit Anuchitanukul · 1996
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 which 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 temporal logic ETL.