Relation algebra and modal logics (Q4362879)

This chapter gives an introduction to modal logics as seen from the context of relation algebra. We illustrate this viewpoint with an example application: verification of reactive systems. This chapter is organized as follows: After defining the logical and relational languages used, we give syntactical translations from modal logic into relation algebra and predicate logic. In Sect. 5.2 we characterize the expressive power of modal formulas and relational terms by bisimulations. Then, in Sect. 5.3 we present some modal completeness and incompleteness results and explicate their implications for the relational language. Finally, Sect. 5.4 on correspondence theory describes a novel way to translate modal axioms into variable-free relation algebraic terms. We conclude with showing how this technique can be applied to more expressive modal languages. For the entire collection see [Zbl 0871.00027].