This thesis studies the problem of automated synthesis of controllers and systems against formal specifications. The two central aims are to study these control problems for branching time specifications and to study them ...