These lectures provide an introduction to modal logic and its use in formalising reasoning about the behaviour of computational processes. They begin with a general introduction to the syntax, semantics, and proof-theory ...