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

- automated verification,
- databases,
- knowledge representation,
- artificial intelligence,
- formal languages,
- etc.

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

- extremely fast implementations of model checkers and tableaux-based and resolution-based theorem provers,
- automata-theoretic methods for deciding powerful languages,
- tight connections between the theories of computational and descriptive complexity,
- and so on.

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

- transition systems,
- parse trees,
- Petri nets,
- decision diagrams,
- flow charts,
- ...

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 .
**