Figure 5: Interleaving semantics ofa|b

This fact creates problems in particular in static analysis of (asynchronous) concurrent systems in that interleaving builds a lot of uninteresting states in the modelisation, hence inducing a high cost in verification. This is called the

Figure 6: A refinement ofa|b

The later semantic papers on the subject were very much influenced by [Pratt, 1991]. In 1992, homological methods (see [Mac Lane, 1963] for a start) for studying the properties of Higher-Dimensional Automata were advocated in [Goubault and Jensen, 1992] given that they provide computable invariants of homotopy (at least in the usual case). A semantics of CCS was also discussed in a suitable category of HDA (also studied in [Lanzmann, 1993]) together with a notion of bisimulation

More general languages were modeled in [Goubault, 1993] with HDAs. Then a few analyses of programs by abstract interpretation ([Cousot and Cousot, 1977] for a start) were designed: some earlier steps in [Cridlig and Goubault, 1993], then the automatic determination of a superset of possible schedules from the geometry of executions (i.e. histories of resource usage) in [Goubault, 1995a] and [Goubault, 1995b], some applications to model-checking in 1995 in [Cridlig, 1995] (for shared-memory programming languages), and in [Cridlig, 1996] (on CML, i.e. message-passing languages). A prototype Parallel Pascal Analyser has been implemented along these lines by R. Cridlig: http://www.dmi.ens.fr/~cridlig.

In ``On the classification of dipaths in geometric models of concurrency'' in a forthcoming issue of ``Mathematical Structure in Computer Science'', M. Raussen focusses on the determination of the dihomotopy classes in cubical complexes, deadlock detection and serializability (see next section) being only special cases. An algorithm is given for the 2-dimensional case and some ideas are given for solving the general case. In ``Loops, Ditopology and Deadlocks'' in the same issue, L. Fajstrup gives a geometric model of a truly-concurrent PV system of

Some proposals have been made to use the scheduling information obtained from the HDA semantics to derive automatic parallelization algorithms. This has been fully treated for CCS in [Takayama, 1995], [Takayama, 1996].

Some potentially related semantic models are the