How are Modal Logic and Graph Theory related?

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.

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.

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.