Modal logics for programs

Abstract

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 of modal languages, and their historical origins. There then follows an exposition of some particular formalisms that are particularly relevant to computer science: dynamic logic, the temporal logic of concurrency, the Hennessy­-Milner logic of processes, and the powerful Mu-Calculus that encompasses all of these systems. The third part explains technical methods (canonical models, filtrations) that have been developed to analyse particular logics, and finally, these methods are applied to give a proof of the completeness theorem for linear temporal logic.