Abstract. This thesis presents a framework for the automatic strategy synthesis from quantitative specifications, in order to control autonomous systems. We model systems as turn-based two-player zero-sum stochastic games, which are able to express both stochastic and nondeterministic environmental uncertainty. Given a system model and a specification, we define the strategy synthesis problem as that of finding a strategy for the system that is winning against every environment. Since large, complex systems are typically built from multiple components, we consider the synthesis of strategies for the individual components separately, which can then be composed to a winning strategy for the full system. Modelling interaction between components is facilitated using assume-guarantee rules, which can express contracts such as "maintain the room temperature of at least 20℃, as long as the windows are closed at least 30% of the time." For the synthesis of strategies for the individual components, we develop synthesis algorithms for Boolean combinations of long-run objectives, specifically, maintaining above a threshold (i) a mean-payoff, almost surely; (ii) an expected mean-payoff; (iii) a ratio of rewards, almost surely; or (iv) a ratio of expected rewards. We implement our algorithms in the PRISM-games 2.0 tool and demonstrate their viability on four case studies.