Arrow Logic

Origin. Venema and others developed arrow logic (1990s). Modal logic of transitions/arrows. Combines aspects of relation algebra and modal logic. Models binary relations as first-class objects. Foundation for dynamic semantics and process algebra connections.

Models. Logic where arrows are primitive. Standard modal: nodes with accessibility. Arrow logic: arrows/transitions are the objects. Arrows have source, target; can compose. Models processes, transitions, relations as entities.

Formalism.

Arrow frames: F = (W, C, R, I) where:

W: set of arrows
C ⊆ W³: composition (aCb,c = "a∘b = c")
R ⊆ W²: reversal (aRb = "a is converse of b")
I ⊆ W: identity arrows

Arrow models: M = (F, V) with V: Prop → P(W). Formulas describe sets of arrows.

Operators:

φ ⊗ ψ: there exist composable arrows a,b with a∈⟦φ⟧, b∈⟦ψ⟧, a∘b = current
φ⁻¹: converse arrows
ι: identity arrows
◇φ: "diamond" relation to φ-arrows

Semantics: M, a ⊨ φ ⊗ ψ iff ∃b,c. C(b,c,a) ∧ M,b ⊨ φ ∧ M,c ⊨ ψ M, a ⊨ φ⁻¹ iff ∃b. R(a,b) ∧ M,b ⊨ φ M, a ⊨ ι iff I(a)

Connection to relation algebra: Arrow logic is modal correspondent of relation algebra. Composition, converse, identity match RA operations.

Symbols.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Composition	Sequential
⁻¹	—	Converse	Reverse
ι	U+03B9	Identity	Self-loops
◇	U+25C7	Diamond	Related arrow
□	U+25A1	Box	All related
C	—	Composition	Ternary relation
R	—	Reversal	Converse relation

Metatheory. Arrow logic is decidable (EXPTIME). Bisimulation invariant. Complete axiomatization exists. Relation algebra embeds. More expressive than basic modal logic. Fragments correspond to relation algebra fragments.

Applies to. Process algebra semantics. Automata theory. Dynamic logic foundations. Relation-based reasoning. Category theory connections. Transition systems.

Limitations. Abstract: far from applications. Relation algebra often suffices. Limited tool support. Specialized audience. Composition may not exist (partial). Learning curve from modal logic.