The paper discusses the synthesis of a reactive module with input \( x \) and output \( y \), specified by a linear temporal formula \( \varphi(x, y) \). The authors show that a program satisfying \( \varphi \) exists if and only if the branching time formula \( (\forall x)(\exists y)A\varphi(x, y) \) is valid over all tree models. For the case where all variables range over finite domains, the validity problem is decidable, and an algorithm is presented to construct the program if it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees, which has exponential complexity in the number of pairs but polynomial complexity in the number of states. This leads to a synthesis algorithm with double-exponential complexity in the length of the specification. The paper also introduces a temporal logic extension and discusses the implementability problem, providing conditions for the existence of a program that satisfies the specification. Finally, it presents examples of developing finite-state reactive modules and discusses the emptiness problem for automata on infinite trees, presenting an improved algorithm with deterministic polynomial time complexity in the number of states and exponential complexity in the number of pairs.The paper discusses the synthesis of a reactive module with input \( x \) and output \( y \), specified by a linear temporal formula \( \varphi(x, y) \). The authors show that a program satisfying \( \varphi \) exists if and only if the branching time formula \( (\forall x)(\exists y)A\varphi(x, y) \) is valid over all tree models. For the case where all variables range over finite domains, the validity problem is decidable, and an algorithm is presented to construct the program if it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees, which has exponential complexity in the number of pairs but polynomial complexity in the number of states. This leads to a synthesis algorithm with double-exponential complexity in the length of the specification. The paper also introduces a temporal logic extension and discusses the implementability problem, providing conditions for the existence of a program that satisfies the specification. Finally, it presents examples of developing finite-state reactive modules and discusses the emptiness problem for automata on infinite trees, presenting an improved algorithm with deterministic polynomial time complexity in the number of states and exponential complexity in the number of pairs.