These structures are intended to allow one to talk about ‘all such objects as may be represented in a picture by arrows’, (Venema).
An arrow frame is a frame, $\mathfrak{F} = (W, C, R, I )$, such that $C$ is a ternary relation, (so $C\subseteq W \times W \times W$), $R$ is a binary relation, and $I$ a unary one, so $I\subseteq W$.
The interpretation intended for these relations is similar to the structure of a groupoid, but from a relational point of view.
For $C(a,b,c)$ think $a = b\star c$, ‘the’ composite of $b$ and $c$, but, of course, $a$ need not be uniquely defined by this;
For $R(a,b)$, think $b$ is a ‘reverse’ arrow for $a$;
For $I(a)$ i.e. $a\in I$, think $a$ is an ‘identity arrow’.
This defines a frame by a relational signature. It does not specify any formulae to be satisfied, nor is there a valuation around to give some ‘meaning’ to the structure.
The arrow language follows the general form of the modal languages, but note that there are several ‘arities’ of relation in the structure, so we need several different types of modal operators.
The arrow language is defined by the rule
where the $p$ are the propositional variables, as usual, and in addition
$1'$ is ‘identity’ and is a nullary modality or modal constant;
$\otimes$ (an unfortunate notation, but which seems fairly standard in the sources used for this) is the ‘converse’ operator and is a ‘diamond’, i.e. a unary operator, and
$\circ$ is the ‘composition operator’ and is a dyadic operator.
The possible interpretations or readings of these include
$1'$ is SKIP;
$\otimes \phi$ is $phi$ conversely; and
$\phi\circ \psi$ is ‘first $\phi$ then $\psi$’.
The usual rules for modal semantics apply. An arrow model, $\mathfrak{M}$, consists of an arrow frame, $\mathfrak{F} = (W, C, R, I )$, (and a valuation $V$, which plays a somewhat behind the scenes role in this general situation). In what follows, $a\in W$,
$\mathfrak{M},a \models 1'$ if and only if $Ia$;
$\mathfrak{M},a \models \otimes\phi$ if and only if $\mathfrak{M},b \models\phi$ for some $b$ with $R a b$;
$\mathfrak{M},a \models\phi\circ \psi$ if and only if $\mathfrak{M},b \models\phi$ and $\mathfrak{M},c \models\psi$ for some $b,c$ with $C a b c$.
A general treatment of these ideas can be found in
whilst a short introduction is