  Reactive synthesis is an automatic way to translate a human intention
expressed in some logic into a system of some kind. This thesis has two parts,
devoted to logic and to systems.
  In Part I, we develop two new approaches to CTL* synthesis. The first
approach consists of two extensions of the SMT-based bounded synthesis: one
follows bottom-up CTL* model checking, another one follows the automata
framework. The second approach reduces CTL* synthesis to LTL synthesis. The
reduction turns any LTL synthesiser into a CTL* synthesiser. The two approaches
were implemented and are available online.
  In Part II, we study parameterized synthesis for two system architectures.
The first architecture is guarded systems and is inspired by cache coherence
protocols. In guarded systems, processes transitions are enabled or disabled
depending on the existence of other processes in certain local states. The
existing cutoff results for guarded protocols are restricted to closed systems,
and are of limited use for liveness properties. We close these gaps and prove
tight cutoffs for open systems with liveness properties, and also cutoffs for
detecting deadlocks. The second architecture is token-ring systems, where the
single token circulates processes arranged in a ring. The experiments with the
existing parameterized synthesis method showed that it does not scale to large
specifications. First, we optimize the method by refining the cutoff reduction,
using modularity and abstraction. The evaluation show several orders of
magnitude speed-ups. Second, we perform parameterized synthesis case study on
the industrial arbiter protocol AMBA. We describe new tricks ---a new cutoff
extension and decompositional synthesis--- that, together with the previously
described optimizations, allowed us to synthesize AMBA in a parameterized
setting, for the first time.
