Relation Algebra and Modal Logics

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. In the design of safety-critical software systems formal semantics and proofs are mandatory. Whereas for functional systems (computing a certain function) usually denotational semantics and Hoare-style reasoning is employed, reactive systems (reacting to an environment) mostly are modelled in an automata-theoretic framework, with a modal or temporal logic proof system. Much of the success of these logics in the specification of reactive systems is due to their ability to express properties without explicit use of first-order variables. For example, consider a program defined by the following transition system: