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)
Best Answer
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.