The connections between logic and computing are wide-spread and varied. Well-known examples of uses of logic in computer science include

Going in the opposite direction, from computer science to logic, we find

And this is just a small part of a far bigger development, as logic continues to play an important role in computer science and permeating more and more of its main areas.

All signs indicate that computer science and logic have decided to establish a stronghold together and profit from the interchange of ideas.

While the links between computer science and modal logic may be viewed as nothing more than specific instances of these developments, there is something special to them. Graphs are the key. Graphs are ubiquitous in computer science: think of

It is because of this, that modal languages are so well suited to describe computer science phenomena: Kripke models, the standard semantic structure on which modal languages are interpreted, are nothing but graphs. Of course, graphs, or more generally relational structures, are also the semantic structures of choice for other languages, including first-order logic, but from a computational point of view, modal languages have a huge advantage when compared to first-order logic: they are usually decidable.