The module is a continuation of the lecture series by Prakash Panangaden on Labelled Markov Processes, but can be independently followed.