Covering space theory for directed topology

TL;DR

This paper explores how covering space theory can be applied to directed topology to analyze state spaces of machines, especially in the presence of loops, by extending geometric techniques from static analysis to looping processes.

Contribution

It introduces a covering space approach for locally preordered geometric realizations of precubical sets, enabling analysis of looping processes in directed topology.

Findings

Locally preordered geometric realizations admit a 'locally monotone' covering.

This covering exists in cases where time does not loop, aiding analysis.

Potential extension of geometric techniques to looping processes in static analysis.

Abstract

The state space of a machine admits the structure of time. For example, the geometric realization of a precubical set, a generalization of an unlabeled asynchronous transition system, admits a "local preorder" encoding control flow. In the case where time does not loop, the "locally preordered" state space splits into causally distinct components. The set of such components often gives a computable invariant of machine behavior. In the general case, no such meaningful partition could exist. However, as we show in this note, the locally preordered geometric realization of a precubical set admits a "locally monotone" covering from a state space in which time does not loop. Thus we hope to extend geometric techniques in static program analysis to looping processes.