Hopscotch—reaching the target hop by hop

• We study algebras for the verification of routing protocols in wireless networks.
• We treat matrices that carry routing information, such as the “next hop” on a path towards a destination.
• By this, we can use algebra not only for determining the length of paths, but also the concrete paths.
• We show how paths can be reconstructed from these matrices, hop by hop.
• Last, we further sketch an application for message passing in wireless networks.

Concrete and abstract relation algebras have widespread applications in computer science. One of the most famous is graph theory. Classical relations, however, only reason about connectivity, not about the length of a path between nodes. Generalisations of relation algebra, such as the min-plus algebra, use numbers allowing the treatment of weighted graphs. In this way one can for example determine the length of shortest paths (e.g. Dijkstra's algorithm). In this paper we treat matrices that carry even more information, such as the “next hop” on a path towards a destination. In this way we can use algebra not only for determining the length of paths, but also the concrete path. We show how paths can be reconstructed from these matrices, hop by hop. We further sketch an application for message passing in wireless networks.