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.

The workshop series Methods for Modalities (M4M) aims to bring together researchers interested in developing algorithms, verification methods and tools based on modal logic. Here the term “modal logic” is conceived broadly, including description logic, guarded fragments, conditional logic, temporal and hybrid logic, etc.

To stimulate interaction and transfer of expertise, M4M will feature a number of invited talks by leading scientists, research presentations aimed at highlighting new developments, and submissions of system demonstrations. We strongly encourage young researchers and students to submit papers, especially for experimental and prototypical software tools which are related to modal logics.