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.
http://www.tac.mta.ca/tac/volumes/22/9/22-09.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/22/9/22-09.pdf