Game models for formal analysis have seen significant research effort over the last two decades. For the analysis of systems with non-deterministic behavior, games are a natural model of choice for studying both co-operative and competitive behaviors of the sources of non-determinism. In game models where the sources of non-determinism are treated adversarially, we have that the properties verified, or refinements synthesized, are correct against all possible realizations of non-deterministic behavior. In areas such as security protocols, where participants are rational and are primarily concerned with achieving their own objectives, and only secondarily concerned with violating the objectives of other participants, games are a natural model of participant behaviors. There is active ongoing research in both the theory and applications of games for verification, compositional reasoning and synthesis. In this dissertation, we first develop the theory of approximate behavioral equivalence and refinement in stochastic games and next explore games for synthesis in two different domains. The first in the automatic synthesis of fair non-repudiation protocols, a subclass of fair exchange protocols, used in e-commerce and the second in synthesizing resource managers that ensure progress, and hence lack of starvation, in multi-threaded C programs. Our results are derived from ideas in probabilistic systems, Markov decision processes and stochastic games.