The paper presents a method for synthesizing a reactive module based on a linear temporal formula φ(x,y). It shows that a program satisfying φ exists if and only if a branching time formula (∀x)(∃y)Aφ(x,y) is valid over all tree models. For finite domains, this problem is decidable, and an algorithm is provided to construct the program. The algorithm uses a new procedure for checking the emptiness of Rabin automata on infinite trees, leading to a synthesis algorithm with double exponential complexity in the specification length. The approach is based on the AE-paradigm, where the synthesis of a program is equivalent to proving the validity of the formula (∀x)(∃y)φ(x,y). This formula is interpreted in branching time logic, where x and y are sequences of values over the computation. The paper discusses the synthesis of both synchronous and asynchronous programs, but focuses on synchronous programs for simplicity. The paper introduces a general branching time temporal logic, including static and dynamic variables, and defines the semantics of state and path formulas. It then defines the implementability problem, showing that a program P satisfies a linear temporal specification φ(x,y) if every behavior of P satisfies φ(x,y). The paper proves that the specification φ(x,y) is implementable if and only if the branching time formula (∀x)(∃y)Aφ(x,y) is valid over all tree models. For the finite-state case, the paper presents an algorithm that constructs a deterministic transducer from a propositional formula. The algorithm reduces the problem to checking the emptiness of a Rabin automaton on infinite trees, which is done in deterministic polynomial time in the number of states and exponential in the number of pairs in the acceptance condition. The synthesis process can be performed in deterministic time that is doubly exponential in the size of the specification. The paper also discusses examples of reactive modules, including a responder and another responder, and presents automata for these examples. It concludes with a discussion of formal languages and automata, and the emptiness problem for automata on infinite trees. The paper shows that the emptiness problem for automata on infinite trees is decidable and presents an algorithm that runs in deterministic polynomial time in the number of states and pairs.The paper presents a method for synthesizing a reactive module based on a linear temporal formula φ(x,y). It shows that a program satisfying φ exists if and only if a branching time formula (∀x)(∃y)Aφ(x,y) is valid over all tree models. For finite domains, this problem is decidable, and an algorithm is provided to construct the program. The algorithm uses a new procedure for checking the emptiness of Rabin automata on infinite trees, leading to a synthesis algorithm with double exponential complexity in the specification length. The approach is based on the AE-paradigm, where the synthesis of a program is equivalent to proving the validity of the formula (∀x)(∃y)φ(x,y). This formula is interpreted in branching time logic, where x and y are sequences of values over the computation. The paper discusses the synthesis of both synchronous and asynchronous programs, but focuses on synchronous programs for simplicity. The paper introduces a general branching time temporal logic, including static and dynamic variables, and defines the semantics of state and path formulas. It then defines the implementability problem, showing that a program P satisfies a linear temporal specification φ(x,y) if every behavior of P satisfies φ(x,y). The paper proves that the specification φ(x,y) is implementable if and only if the branching time formula (∀x)(∃y)Aφ(x,y) is valid over all tree models. For the finite-state case, the paper presents an algorithm that constructs a deterministic transducer from a propositional formula. The algorithm reduces the problem to checking the emptiness of a Rabin automaton on infinite trees, which is done in deterministic polynomial time in the number of states and exponential in the number of pairs in the acceptance condition. The synthesis process can be performed in deterministic time that is doubly exponential in the size of the specification. The paper also discusses examples of reactive modules, including a responder and another responder, and presents automata for these examples. It concludes with a discussion of formal languages and automata, and the emptiness problem for automata on infinite trees. The paper shows that the emptiness problem for automata on infinite trees is decidable and presents an algorithm that runs in deterministic polynomial time in the number of states and pairs.