5 - Basic Modal Logics

Summary

This chapter is a brief introduction to the basic multimodal logic BML, interpreted as the simplest natural temporal logic for reasoning about transition systems. Indeed, transition systems are nothing but Kripke frames and interpreted transition systems are simply Kripke models, so a standard Kripke semantics is provided for a multimodal language with modal operators □_a and ◊_a, associated with each transition relation R_a. These bear natural meaning in interpreted transition systems, stating what must be true in all /respectively, what may be true at some/ R_a-successors of the current state. In order to emphasise these readings of the modal operators, we will use a notation that is unusual for modal logic, but is more suitable in the context of temporal logics: AX_a (read as for all paths starting from the current state, at the next state) and EX_a (for some path starting from the current state, at the next state). Thus, BML is the minimal natural logical language to specify local properties of transition systems.

Since the chapter is written from the primary perspective of transition systems, rather than from modal logic perspective, we have put an emphasis on certain topics such as expressiveness, bisimulation, model checking, the finite model property and deciding satisfiability, while other fundamental topics in modal logic – such as deductive systems and proof theory, model theory, correspondence theory, algebraic semantics and duality theory – are almost left untouched here. Of all deductive systems developed for modal logics we only mention the axiomatic system for BML here and present a version of the tableaubased method for it in Chapter 13; for the rest we only provide basic references in the bibliographic notes.

This chapter can also be viewed as a stepping stone towards the more expressive and interesting temporal logics that are presented further.

Structure of this chapter. Section 5.1 presents the syntax and semantics for BML. The relational translation from BML into first-order logic (FO) is also presented emphasising the fact that BML can be viewed as a fragment of classical first-order predicate logic. Section 5.2 presents some techniques for renaming and transformation of BML formulae to equisatisfiable ones in certain normal form of modal depth two.