In this talk, I will introduce and motivate a well-studied probabilistic variant of the classic inclusion problem between formal languages. Also known as probabilistic model checking, the problem asks to determine the probability that a word drawn randomly from some known probability measure L (often modelling the behaviour of a system to be verified) is contained in a target language M (modelling the desired system specification). As in the traditional setting, probabilistic language inclusion is typically studied through the lens of automata theory. A generative variant of probabilistic automata (which is closely related to Markov chains) is employed to model probability measures on infinite words. A variety of problems arise by considering automata models with different expressive power, acceptance conditions, etc. The standard approach for solving such problems relies on determinizing the automaton for the target language M, an automata-theoretic product construction, and a numerical analysis of the resulting Markov chain-like stochastic process. I will demonstrate this solution approach with the example of probabilistic pushdown automata and omega-visibly pushdown languages.