Covering space theory for directed topology

Eric Goubault, Emmanuel Haucourt, Sanjeevi Krishnan

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.

Keywords: pospace, covering space, directed topology

2000 MSC: 54E99, 54F05, 68N30, 68Q85

Theory and Applications of Categories, Vol. 22, 2009, No. 9, pp 252-268.

TAC Home