Abstract. Probabilistic model checking is a formal verification technique for systems that exhibit stochastic behaviour. It has been used to analyse a wide range of systems, including communication protocols, such as Bluetooth and FireWire, randomised security protocols, e.g. for anonymity and contract signing, and many others. This paper gives a short introduction to probabilistic model checking, with a particular focus on systems that incorporate real-time behaviour. We describe the model of probabilistic timed automata (PTAs), which can be used to represent systems with both probabilistic and real-time characteristics. We illustrate how to formally specify quantitative properties of PTAs, and give a brief summary of the techniques and tools that can be used to verify them. Pointers are provided throughout to further reading on this and related topics.