Concurrency theory in Computer Science studies the effects that arise when several processors run simultaneously sharing common resources. It attempts to advise methods to deal with the "state space explosion problem". In recent years, models with a combinatorial/topological flavor have been introduced and investigated as tools in the analysis of concurrent processes. It is a common feature of these models that an execution corresponds to a directed path (d-path), and that d-homotopies (preserving the directions) have equivalent computations as a result.

I will discuss a particular classical example of a directed space arising as a (pre-cubical set) model of a class of Higher Dimensional Automata (HDA). For such a space, I will describe a new method that determines the homotopy type of the space of traces (executions) as a prodsimplicial complex - with products of simplices as building blocks. A description of that complex opens up for (machine) calculations of homology groups and other topological invariants of the trace space. The determination of path components is particularly important for applications.

This prodsimplicial trace complex arises from a covering of a trace space by particular contractible subspaces. Nonempty (and contractible) intersections of these subspaces form a poset category with a classifying space that corresponds to a barycentric subdivision of the prodsimplicial complex.

The determination of this complex in a particular case depends on deciding whether certain subspaces of traces are empty are not. This decision relies on an algorithm detecting deadlocks and unsafe regions for these Higher Dimensional Automata by checking a bunch of inequalities.

This concept is the background for an algorithm yielding a representation of the prodsimplicial complex that has been implemented using the ALCOOL software from a lab at CEA in France. Using the outcome of the algorithm, homological invariants have been calculated using homology software by Mrozek etal.

If time permits, I will sketch a method that generalizes the main construction to arbitrary HDA taking into account processes that may branch and loop.