Covering space theory for directed topology
Éric Goubault, Emmanuel Haucourt, Sanjeevi Krishnan · Theory and applications of categories · 2009
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.