We study a class of games introduced by Mio to capture the probabilistic μ-calculi called branching games. They are a subclass of stochastic two-player zero-sum turn-based infinite-time games of imperfect information. Branching games extend Gale-Stewart games by allowing players to split the execution of a play into new concurrent sub-games that continue their execution independently. In consequence, the play of a branching game has a tree-like structure, as opposed to linearly structured plays of Gale-Stewart games.In this thesis, we focus our attention on regular branching games. Those are the branching games whose pay-off functions are the indicator functions of regular sets of infinite trees, i.e. the sets recognisable by finite tree au...