Global view on reactivity: switch graphs and their logics

The notion of reactive graph generalises the one of graph by allowing the
base accessibility relation to change when its edges are traversed. Can we represent these more general structures using points and arrows? We prove this can be done
by introducing higher order arrows: the switches.
The possibility of expressing the dependency of the future states of the accessibility relation on individual transitions by the use of higher-order relations,
that is, coding meta-relational concepts by means of relations, strongly suggests the use of
modal languages to reason directly about these structures. We introduce a hybrid
modal logic for this purpose and prove its completeness.