How are Modal Logic and Graph Theory related? I am currently taking a graduate logic course on Modal Logic and I can't help notice that there are a certain class of graphs characterized by the modal axioms such as (4) $\Box p \rightarrow \Box \Box p$, (5) $\Diamond p \rightarrow \Box \Diamond p$, or (B) $p \rightarrow \Box \Diamond p$ which can characterize frames as being transitive, Euclidean, and symmetric, respectively. In general, I notice many similarities between the models used in Modal Logic and the graphs in Graph Theory and I'm wondering if anyone knows if there are applications of Modal Logic to Graph Theory, or if one subject might be a special case of the other?
In any case, if anyone has studied this before or knows of any references on the interplay between Modal Logic and Graph Theory I would be very interested to read about it, and if it has not been studied before then I would be interested of any ideas regarding what open research problems could be stated to tackle the correspondence between these two topics. (A category theory perspective on this interplay would also be very interesting)
 A: On page 724 the book "Handbook of Modal Logic" contains the phrase "modal logics are merely sublogics of appropriate monadic second-order logic" therefore you might be interested in the book "Graph Structure and Monadic Second-Order Logic" by Bruno Courcelle and Joost Engelfriet.
A: Maybe look at arrow logic?
A: The relationship between modal logic and graph theory has, indeed, been studied before. Peter mentioned sheaf models in the comments; I want to mention a more classical-logic-y perspective.
(First, let me note that when we say that $\phi$ characterizes a class of frames $V$, we mean that for every frame in $V$, and every valuation on that frame, $\phi$ is true, i.e., $\phi$ is a validity on every frame in $V$. There are frames together with valuations which satisfy, e.g., $\square p\implies \square \square p$ without the frame being transitive.)
It's a natural question to ask which properties of frames can be defined by propositional modal formulas. For example, as you mentioned in the question, we can characterize transitivity by a single modal formula. It turns out that the class of properties of frames which can be captured by modal formulas is substantially larger than the class of first-order-definable properties. Blackburn, de Rijke, and Venema's book ("Modal logic") gives the example of the Lob formula: $$ \square (\square p\implies p)\implies \square p$$ They show that this formula is a validity in precisely those frames in which the relation $R$ is transitive and well-founded (although they use the term "converse well-founded"). By a compactness argument, this class of frames is not first-order axiomatizable. A result of Goldblatt and Thomason in 1974 showed that "a first-order frame property is modally definable iff it is preserved under taking generated subframes, p-morphic frame images, disjoint unions, and inverse ultrafilter extensions." I don't really understand what all that means, but at the very least we can take away that not every first-order property of frames is characterized by a (propositional) modal formula.
In the other direction, since the definition of "valid modal formula" is second-order, it's clear that any class of frames which can be captured by a modal formula is definable in second-order logic. I recall a paper on the strength of modal logic that showed that a sort of converse to this held, despite the converse itself failing (since, as mentioned above, not even every first-order property of frames is modally definable) but I can't track it down at the moment. EDIT: Emil found it - it's "Reduction of second-order logic to modal logic" by S. K. Thomason, and a (very poor) copy can be found here: http://onlinelibrary.wiley.com/doi/10.1002/malq.19750210114/abstract.
In general, the book "Modal logics" by Chagrov and Zakharyaschev is probably the book to look at. I don't know how up-to-date it is anymore, but it seems to include every perspective on modal logics that I've heard of, short of the category-theoretic aspects.
EDIT: Another aspect, which I didn't think of at first, is given by alternate interpretations of modalities. For example, suppose we interpret $\square p$ as meaning "more than half of visible nodes satisfy $p$," instead of "all visible nodes satisfy $p$;" or some other interpretation. Under each interpretation, the classes of graphs we can charaterize by modal formulas changes; and while any specific alternate interpretation is probably not too interesting, general tools for studying that would probably be very deep and valuable. I don't know of any work on this, but I suspect it's been done before; the closest related source I can find at present is the extended abstract of "The Modal Logic of Probability" (Heifetz, Mongin) which seems vaguely along these lines.
A: The ability of modal assertions to define natural and interesting
classes of frames (or digraphs) is indeed intensely studied and
constitutes one of the principal perpsectives of the subject,
pervasive in all the literature and textbooks. Indeed, I heard
Blackburn assert at a conference talk last fall that one
should think about modal assertions mainly as a way of
describing certain classes of graphs.
Any of the standard reference texts on modal logic will tell you
that:


*

*the modal theory S5 characterizes the equivalence relations;

*the modal theory S4.3 characterizes the linear pre-orders; 

*the modal theory S4.2 characterizes the directed partial pre-orders;

*the modal theory S4 characterizes the partial pre-orders;

*And so on.


There are numerous instances of this phenomenon for various
logics, and modal logicians are particularly interested in logics
with the finite frame property, which are those definable as
arising from a class of finite frames.
In some of my recent work, Structural connections between a forcing class and its modal logic, for example, we have been looking
at all those logics and also what we call S4.tBA,
topless-Boolean-algebra logic, which is characterized as the
assertions true in every finite topless pre-Boolean algebra (a
finite pre-Boolean algebra whose maximal cluster has been removed). We keep being pushed toward the idea that this may be the modal logic of class forcing, and also of c.c.c. forcing. The
connection between the modal assertions and the nature of the
frames is exploited throughout the work.
