Uli Fahrenberg

Fabrizio Biondi

Kevin Corre

Cyrille Jegourel

Simon Kongshøj

Axel Legay

Measuring Global Similarity between Texts

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Statistical approaches for comparing texts are used for example in machine translation for assessing the quality of machine translation tools [START_REF] Lin | Automatic evaluation of summaries using n-gram co-occurrence statistics[END_REF][START_REF] Lin | Automatic evaluation of machine translation quality using longest common subsequence and skip-bigram statistics[END_REF][START_REF] Papineni | BLEU: a method for automatic evaluation of machine translation[END_REF], or in computational linguistics in order to establish authorship [START_REF] Cortelazzo | Improving Labbé's intertextual distance: Testing a revised version on a large corpus of italian literature[END_REF][START_REF] Labbé | Inter-textual distance and authorship attribution. Corneille and Molière[END_REF][START_REF] Labbé | Experiments on authorship attribution by intertextual distance in English[END_REF][START_REF] Savoy | Authorship attribution: A comparative study of three text corpora and three languages[END_REF][START_REF] Savoy | Authorship attribution based on specific vocabulary[END_REF][START_REF] Tomasi | Towards a taxonomy of suspected forgery in authorship attribution field. A case: Montale's Diario Postumo[END_REF] or to detect "fake", i.e., automatically generated, scientific papers [START_REF] Labbé | Duplicate and fake publications in the scientific literature: how many SCIgen papers in computer science?[END_REF][START_REF] Noorden | Publishers withdraw more than 120 gibberish papers[END_REF].

Generally speaking, these approaches consist in computing distances, or similarity measures, between texts and then using statistical methods such as, for instance, hierarchical clustering [START_REF] Kaufman | Finding Groups in Data: An Introduction to Cluster Analysis[END_REF] to organize the distance data and draw conclusions.

The distances between texts which appear to be the most popular, e.g., [START_REF] Labbé | Inter-textual distance and authorship attribution. Corneille and Molière[END_REF][START_REF] Papineni | BLEU: a method for automatic evaluation of machine translation[END_REF], are all based on measuring differences in 1-gram frequencies: For each 1-gram (token, or word) w in the union of A and B, its absolute frequencies in both texts are calculated, i.e., F A (w) and F B (w) are the numbers of occurrences of w in A and B, respectively, and then the distance between A and B is defined to be the sum, over all words w in the union of A and B, of the absolute differences |F A (w) -F B (w)|, divided by the combined length of A and B for normalization. When the texts A and B have different length, some adjustments are needed; also, some algorithms [START_REF] Lin | Automatic evaluation of summaries using n-gram co-occurrence statistics[END_REF][START_REF] Papineni | BLEU: a method for automatic evaluation of machine translation[END_REF] take into account also 2-, 3-and 4-grams.

These distances are thus based on a local model of the texts: they measure differences of the multisets of n-grams for n between 1 and maximally 4. Borrowing techniques from economics and theoretical computer science, we will propose below a new distance which instead builds on the global structure of the texts. It simultaneously measures differences in occurrences of n-grams for all n and uses a discounting parameter to balance the influence of long n-grams versus short n-grams.

Following the example of [START_REF] Labbé | Duplicate and fake publications in the scientific literature: how many SCIgen papers in computer science?[END_REF], we then use our distance to automatically identify "fake" scientific papers. These are "papers" which are automatically generated by some piece of software and are hence devoid of any meaning, but which, at first sight, have the appearance of a genuine scientific paper.

We can show that using our distance and hierarchical clustering, we are able to automatically identify such fake papers, also papers generated by other methods than the ones considered in [START_REF] Labbé | Duplicate and fake publications in the scientific literature: how many SCIgen papers in computer science?[END_REF], and that, importantly, some parts of the analysis become more reliable the higher the discounting factor. We conclude that measuring global differences between texts, as per our method, can be a more reliable way than the current state-of-the-art methods to automatically identify fake scientific papers. We believe that this also has applications in other areas such machine translation or computational linguistics.

Inter-textual Distances

For the purpose of this paper, a text A is a sequence A = (a 1 , a 2 , . . . , a N A ) of words. The number N A is called the length of A. As a vehicle for showing idealized properties, we may sometimes also speak of infinite texts, but most commonly, texts are finite and their length is a natural number. Note that we pay no attention to punctuation, structure such as headings or footnotes, or non-textual parts such as images.

1-gram distance

Before introducing our global distance, we quickly recall the definition of standard 1-gram distance, which stands out as a rather popular distance in computational linguistics and other areas [3, 14-17, 24, 25, 30].

For a text A = (a 1 , a 2 , . . . , a N A ) and a word w, the natural number F A (w) = |{i | a i = w}| is called the absolute frequency of w in A: the number of times (which may be 0) that w appears in A. We say that w is contained in A and write w ∈ A if F A (w) ≥ 1.

For texts

A = (a 1 , a 2 , . . . , a N A ), B = (b 1 , b 2 , . . . , b N B ), we write A • B = (a 1 , . . . , a N A , b 1 , . . . , b N B )
for their concatenation. With this in place, the 1-gram distance between texts A and B of equal length is defined to be

d 1 (A, B) = w∈A•B |F A (w) -F B (w)| N A + N B ,
where |F A (w) -F B (w)| denotes the absolute difference between the absolute frequencies F A (w) and F B (w).

For texts A and B which are not of equal length, scaling is used: for N A < N B , one lets

d 1 (A, B) = w∈A•B |F A (w) -F B (w) N A N B | 2N A .
By counting occurrences of n-grams instead of 1-grams, similar n-gram distances may be defined for all n ≥ 1. The BLEU distance [START_REF] Papineni | BLEU: a method for automatic evaluation of machine translation[END_REF] for example, popular for evaluation of machine translation, computes n-gram distance for n between 1 and 4.

Global distance

To compute our global inter-textual distance, we do not compare word frequencies as above, but match n-grams in the two texts approximately. Let A = (a 1 , a 2 , . . . , a N A ) and B = (b 1 , b 2 , . . . , b N B ) be two texts, where we make no assertion about whether

N A < N B , N A = N B or N A > N B . Define an indicator function δ i,j , for i ∈ {1, . . . , N A }, j ∈ {1, . . . , N B }, by δ i,j = 0 if a i = b j , 1 otherwise (1)
(this is the Kronecker delta for the two sequences A and B). The symbol δ i,j indicates whether the i-th word a i in A is the same as the j-th word b j in B.

For ease of notation, we extend δ i,j to indices above i, j, by declaring

δ i,j = 1 if i > N A or j > N B .
Let λ ∈ R, with 0 ≤ λ < 1, be a discounting factor. Intuitively, λ indicates how much weight we give to the length of n-grams when matching texts: for λ = 0, we match 1-grams only (see also Theorem 1 below), and the higher λ, the longer the n-grams we wish to match. Discounting is a technique commonly applied for example in economics, when gauging the long-term effects of economic decisions. Here we remove it from its time-based context and apply it to n-gram length instead: We define the position match from any position index pair (i, j) in the texts by

d pm (i, j, λ) = δ i,j + λδ i+1,j+1 + λ 2 δ i+2,j+2 + • • • = ∞ k=0 λ k δ i+k,j+k . (2)
This measures how much the texts A and B "look alike" when starting with the tokens a i in A and b j in B. Note that it takes values between 0 (if a i and b j are the starting points for two equal infinite sequences of tokens) and 1 1-λ . Intuitively, the more two token sequences are alike, and the later they become different, the smaller their distance. Table 1 shows a few examples of position match calculations. This gives us an N A -by-N B matrix D pm (λ) of position matches; see Table 2 for an example. We now need to consolidate this matrix into one global distance value between A and B. Intuitively, we do this by averaging over position matches: for each position a i in A, we find the position b j in B which best matches a i , i.e., for which d pm (i, j, λ) is minimal, and then we average over these matchings.

Formally, this can be stated as an assignment problem: Assuming for now that N A = N B , we want to find a matching of indices i to indices j which minimizes the sum of the involved d pm (i, j). Denoting by S N A the set of all permutations of indices {1, . . . , N A } (the symmetric group on N A elements), we hence define This is a conservative extension of 1-gram distance, in the sense that for discounting factor λ = 0 we end up computing d 1 :

d 2 (A, B, λ) = (1 -λ) 1 N A min φ∈S N A N A i=1 d pm (i, φ(i), λ) .
Theorem 1. For all texts A, B with equal lengths, d 2 (A, B, 0) = d 1 (A, B).
Proof. For λ = 0, the entries in the phrase distance matrix are d pm (i, j, 0) = δ i,j . Hence a perfect match in D pm , with

N A i=1 d pm (i, φ(i), 0) = 0,
matches each word in A with an equal word in B and vice versa. This is possible if, and only if,

F A (w) = F B (w) for each word w. Hence d 2 (A, B, 0) = 0 iff d 1 (A, B) = 0. The proof of the general case is in appendix.
There are, however, some problems with the way we have defined d 2 . For the first, the assignment problem is computationally rather expensive: the best know algorithm (the Hungarian algorithm [START_REF] Kuhn | The Hungarian method for the assignment problem[END_REF]) runs in time cubic in the size of the matrix, which when comparing large texts may result in prohibitively long running times. Secondly, and more important, it is unclear how to extend this definition to texts which are not of equal length, i.e., for which N A = N B . (The scaling approach does not work here.)

Hence we propose a different definition which has shown to work well in practice, where we abandon the idea that we want to match phrases uniquely. In the definition below, we simply match every phrase in A with its best equivalent in B, and we do not take care whether we match two different phrases in A with the same phrase in B. Hence, the quick fox jumps over the lazy dog the 0.67 1.00 1.00 1.00 1.00 0.64 1.00 1.00 lazy 1.00 0.84 1.00 1.00 1.00 1.00 0.80 1.00 fox 1.00 1.00 0.80 1.00 1.00 1.00 1.00 1.00

d 3 (A, B, λ) = 1 N A N A i=1 min j=1,...,N B d pm (i, j, λ) .
Note that d 3 (A, B, λ) ≤ d 2 (A, B, λ), and that contrary to d 2 , d 3 is not symmetric. We can fix this by taking as our final distance measure the symmetrization of d 3 :

d 4 (A, B, λ) = max(d 3 (A, B, λ), d 3 (B, A, λ)) .

Implementation

We have written a C program and some bash helper scripts which implement the computations above. All our software is available at http://textdist.gforge.inria.fr/. The C program, textdist.c, takes as input a list of txt-files A 1 , A 2 , . . . , A k and a discounting factor λ and outputs d 4 (A i , A j , λ) for all pairs i, j = 1, . . . , k. With the current implementation, the txt-files can be up to 15,000 words long, which is more than enough for all texts we have encountered. On a standard 3-year-old business laptop (Intel R Core TM i5 at 2.53GHz×4), computation of d 4 for takes less than one second for each pair of texts.

We preprocess texts to convert them to txt-format and remove non-word tokens. The bash-script preprocess-pdf.sh takes as input a pdf-file and converts it to a text file, using the poppler library's pdftotext tool. Afterwards, sed and grep are used to convert whitespace to newlines and remove excessive whitespace; we also remove all "words" which contain non-letters and only keep words of at least two letters.

The bash-script compareall.sh is used to compute mutual distances for a corpus of texts. Using textdist.c and taking λ as input, it computes d 4 (A, B, λ) for all texts (txt-files) A, B in a given directory and outputs these as a matrix. We then use R and gnuplot for statistical analysis and visualization.

We would like to remark that all of the above-mentioned tools are free or open-source software and available without charge. One often forgets how much science has come to rely on this free-software infrastructure.

Experiments

We have conducted two experiments using our software. The data sets on which we have based these experiments are available on request.

Types of texts used

We have run our experiments on papers in computer science, both genuine papers and automatically generated "fake" papers. As to the genuine papers, for the first experiment, we have used 42 such papers from within theoretical computer science, 22 from the proceedings of the FORMATS 2011 conference [START_REF]Formal Modeling and Analysis of Timed Systems -9th Int. Conf[END_REF] and 20 others which we happened to have around. For the second experiment, we collected 100 papers from arxiv.org, by searching their Computer Science repository for authors named "Smith" (arxiv.org strives to prevent bulk paper collection), of which we had to remove three due to excessive length (one "status report" of more than 40,000 words, one PhD thesis of more than 30,000 words, and one "road map" of more than 20,000 words).

We have employed three methods to collect automatically generated "papers". For the first experiment, we downloaded four fake publications by "Ike Antkare". These are out of a set of 100 papers by the same "author" which have been generated, using the SCIgen paper generator, for another experiment [START_REF] Labbé | Ike Antkare, one of the great stars in the scientific firmament[END_REF]. For the purpose of this other experiment, these papers all have the same bibliography, each of which references the other 99 papers; hence not to skew our results (and like was done in [START_REF] Labbé | Duplicate and fake publications in the scientific literature: how many SCIgen papers in computer science?[END_REF]), we have stripped their bibliography.

SCIgen3 is an automatic generator of computer science papers developed in 2005 for the purpose of exposing "fake" conferences and journals (by submitting generated papers to such venues and getting them accepted). It uses an elaborate grammar to generate random text which is devoid of any meaning, but which to the untrained (or inattentive) eye looks entirely legitimate, complete with abstract, introduction, figures and bibliography. For the first experiment, we have supplemented our corpus with four SCIgen papers which we generated on their website. For the second experiment, we modified SCIgen so that we could control the length of generated papers and then generated 50 papers.

For the second experiment, we have also employed another paper generator which works using a simple Markov chain model. This program, automogensen 4 , was originally written to expose the lack of meaning of many of a certain Danish political commentator's writings, the challenge being to distinguish genuine Mogensen texts from "fake" automogensen texts. For our purposes, we have modified automogensen to be able to control the length of its output and fed it with a 248,000-word corpus of structured computer science text (created by concatenating all 42 genuine papers from the first experiment), but otherwise, its functionality is rather simple: It randomly selects a 3-word starting phrase from the corpus and then, recursively, selects a new word from the corpus based on the last three words in its output and the distribution of successor words of this three-word phrase in the corpus.

First experiment

The first experiment was conducted on 42 genuine papers of lengths between 3,000 and 11,000 words and 8 fake papers of lengths between 1500 and 2200 words. Figure 1 shows two dendrograms with average clustering created from the collected distances; more dendrograms are available in appendix. The left dendrogram was computed for discounting factor λ = 0, i.e., word matching only. One clearly sees the fake papers grouped together in the top cluster and the genuine papers in cluster below. In the right dendrogram, with very high discounting (λ = .95), this distinction is much more clear; here, the fake cluster is created (at height .85) while all the genuine papers are still separate. The dendrograms in Fig. 2, created using Ward clustering, clearly show that one should distinguish the data into two clusters, one which turns out to be composed only of fake papers, the other only of genuine papers. We want to call attention to two other interesting observations which can be made from the dendrograms in Fig. 1. First, papers 2, 21 and 22 seem to stick out from the other genuine papers. While all other genuine papers are technical papers from within theoretical computer science, these three are not. Paper 2 [START_REF] Haverkort | Formal modeling and analysis of timed systems: Technology push or market pull[END_REF] is a non-technical position paper, and papers 21 [START_REF] Sankaranarayanan | Model-based dependability analysis of programmable drug infusion pumps[END_REF] and 22 [START_REF] Kharmeh | A design-for-verification framework for a configurable performance-critical communication interface[END_REF] are about applications in medicine and communication. Note that the λ = .95 dendrogram more clearly distinguishes the position paper [START_REF] Haverkort | Formal modeling and analysis of timed systems: Technology push or market pull[END_REF] from the others. Another interesting observation concerns papers 8 [START_REF] Basset | Thin and thick timed regular languages[END_REF] and 33 [START_REF] Asarin | Volume and entropy of regular timed languages[END_REF]. These papers share an author (E. Asarin) and are within the same specialized area (topological properties of timed automata), but published two years apart. When measuring only word distance, i.e., with λ = 0, these papers have the absolutely lowest distance, .23, even below any of the fake papers' mutual distances, but increasing the discounting factor increases their distance much faster than any of the fake papers' mutual distances. At λ = .95, their distance is .87, above any of the fake papers' mutual distances. A conclusion can be that these two papers may have word similarity, but they are distinct in their phrasing.

V45 V30 V28 V31 V29 V44 V43 V46 V21 V38 V26 V40 V50 V20 V37 V42 V27 V34 V32 V39 V5 V48 V16 V36 V47 V24 V25 V18 V19 V9 V35 V10 V11 V41 V49 V14 V17 V12 V7 V15 V3 V8 V33 V13 V4 V6 V1 V23 V2 V22
Finally, we show in Table 3 (see also Fig. 10 in the appendix for a visualization) how the mutual distances between the 50 papers evolve depending on the discounting factor. One can see that at λ = 0, the three types of mutual distances are overlapping, whereas at λ = .95, they are almost separated into three bands: .81-.86 for fake papers, .86-.90 for genuine papers, and .89-.92 for comparing genuine with fake papers.

Altogether, we conclude from the first experiment that our inter-textual distance can achieve a safe separation between genuine and fake papers in our corpus, and that the separation is stronger for higher discounting factors.

Second experiment

The second experiment was conducted on 97 papers from arxiv.org, 50 fake papers generated by a modified SCIgen program, and 50 fake papers generated by automogensen. The arxiv papers were between 1400 and 15,000 words long, the SCIgen papers between 2700 and 12,000 words, and the automogensen papers between 4,000 and 10,000 words. The distances were computed for discounting factors 0, .4, .8 and .95; with our software, computations took about four hours for each discounting factor.

We show the dendrograms using average clustering in Figs. 11 to 14 in the appendix; they appear somewhat inconclusive. One clearly notices the SCIgen and automogensen parts of the corpus, but the arxiv papers have wildly varying distances and disturb the dendrogram. One interesting observation is that with discounting factor 0, the automogensen papers have small mutual distances compared to the arxiv corpus, comparable to the SCIgen papers' mutual distances, whereas with high discounting (.95), the automogensen papers' mutual distances look more like the arxiv papers'. Note that the difficulties in clustering appear also with discounting factor 0, hence also when only matching words.

The dendrograms using Ward clustering, however, do show a clear distinction between the three types of papers. We can only show one of them here, for λ = .95 in Fig. 3; the rest are available in appendix. One clearly sees the SCIgen cluster (top) separated from all other papers, and then the automogensen cluster (middle) separated from the arxiv cluster.

There is, though, one anomaly: two arxiv papers have been "wrongly" grouped into their own cluster (between the SCIgen and the automogensen clusters). Looking at these papers, we noticed that here our pdf-to-text conversion had gone wrong: the papers' text was all garbled, consisting only of "AOUOO OO AOO EU OO OU AO" etc. The dendrograms rightly identify these two papers in their own cluster; in the dendrograms using average clustering, this garbled cluster consistently has distance 1 to the other clusters.

We also notice in the dendrogram with average clustering and discounting factor .95 (Fig. 14 in the appendix) that some of the arxiv papers with small mutual distances have the same authors and are within the same subject. This applies to [START_REF] Smith | Bayesian discovery of threat networks[END_REF] vs. [START_REF] Smith | Network detection theory and performance[END_REF] and to [START_REF] Ulusoy | Robust multi-robot optimal path planning with temporal logic constraints[END_REF] vs. [START_REF] Ulusoy | Optimal multi-robot path planning with temporal logic constraints[END_REF]. These similarities appear much more clearly in the λ = .95 dendrogram than in the ones with lower discounting factor.

As a conclusion from this experiment, we can say that whereas average clustering had some difficulties in distinguishing between fake and arxiv papers, Ward clustering did not have any problems. The only effect of the discounting factor we could see was in identifying similar arxiv papers. We believe that one reason for the inconclusiveness of the dendrograms with average clustering is the huge variety of the arxiv corpus. Whereas the genuine corpus of the first experiment included only papers from the verification sub-field of theoretical computer science, the arxiv corpus is comprised of papers from a diverse selection of research areas within computer science, including robotics, network detection, computational geometry, constraint programming, numerical simulation and many others. Hence, the intra-corpus variation in the arxiv corpus hides the inter-corpus variations.

Conclusion and Further Work

We believe we have collected enough evidence that our global inter-textual distance provides an interesting alternative, or supplement, to the standard 1-gram distance. In our experiments, we have seen that measuring inter-textual distance with high discounting factor enables us to better differentiate between similar and dissimilar texts. More experiments will be needed to identify areas where our global matching provides advantages over pure 1-gram matching.

With regard to identifying fake scientific papers, we remark that, according to [START_REF] Labbé | Duplicate and fake publications in the scientific literature: how many SCIgen papers in computer science?[END_REF], "[u]sing [the 1-gram distance] to detect SCIgen papers relies on the fact that [...] the SCIgen vocabulary remains quite poor". Springer has recently announced [29] that they will integrate "[a]n automatic SCIgen detection system [...] in [their] submission check system", but they also notice that the "intention [of fake papers' authors] seems to have been to increase their publication numbers and [...] their standing in their respective disciplines and at their institutions"; of course, auto-detecting SCIgen papers does not change these motivations. It is thus reasonable to expect that generators of fake papers will get better, so that also better tools will be needed to detect them. We propose that our phrase-based distance may be such a tool.

There is room for much improvement in our distance definition. For once, we perform no tagging of words which could identify different spellings or inflections of the same word. This could easily be achieved by, using for example the Wordnet database5 , replacing our binary distance between words in Eq. ( 1) with a quantitative measure of word similarity. For the second, we take no consideration of omitted words in a phrase; our position match calculation in Eq. ( 2) cannot see when two phrases become one-off like in "the quick brown fox jumps..." vs. "the brown fox jumps...".

Our inter-textual distance is inspired by our work in [START_REF] Fahrenberg | Generalized quantitative analysis of metric transition systems[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branching-time spectrum[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF] and other papers, where we define distances between arbitrary transition systems. Now a text is a very simple transition system, but so is a text with "one-off jumps" like the one above. Similarly, we can incorporate swapping of words into our distance, so that we would be computing a kind of discounted Damerau-Levenshtein distance [START_REF] Damerau | A technique for computer detection and correction of spelling errors[END_REF] (related approaches, generally without discounting, are used for sequence alignment in bioinformatics [START_REF] Needleman | A general method applicable to the search for similarities in the amino acid sequence of two proteins[END_REF][START_REF] Smith | Identification of common molecular subsequences[END_REF]). We have integrated this approach in an experimental version of our textdist tool. Fig. 10. Distances between all pairs of genuine papers (top), all pairs of fake papers (middle), and between genuine and fake papers (bottom) in Experiment 1, depending on the discounting factor. Lines between points have been added for visualization. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

V28 V31 V30 V45 V43 V46 V29 V44 V21 V2 V22 V38 V40 V50 V26 V37 V42 V32 V39 V20 V48 V16 V5 V4 V6 V13 V36 V27 V34 V47 V24 V25 V18 V19 V14 V15 V49 V9 V11 V10 V35 V41 V1 V23 V17 V3 V8 V33 V7 V12

Fig. 3 .

 3 Fig. 3. Dendrogram for Experiment 2, using Ward clustering, for discounting factor .95. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

Fig. 11 .Fig. 12 . 4 .Fig. 13 . 8 .Fig. 14 .

 1112413814 Fig. 11. Dendrogram for Experiment 2, using average clustering, for discounting factor 0. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

Fig. 15 .

 15 Fig. 15. Dendrogram for Experiment 2, using Ward clustering, for discounting factor 0. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

Fig. 16 .

 16 Fig. 16. Dendrogram for Experiment 2, using Ward clustering, for discounting factor .4. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

Fig. 17 .

 17 Fig. 17. Dendrogram for Experiment 2, using Ward clustering, for discounting factor .8. Black dots mark arxiv papers, green marks SCIgen papers, and automogensen papers are marked red.

Table 1 .

 1 Position matches, starting from index pair (1, 1) and scaled by 1 -λ, of different example texts, for general discounting factor λ and for λ = .8. Note that the last two example texts are infinite.

	Text A	Text B	(1 -λ)dpm(1, 1, λ) λ = .8
	"man"	"dog"	1	1
	"dog"	"dog"	λ	.8
	"man bites dog"	"man bites dog"	λ 3	.51
	"man bites dog"	"dog bites man"	1 -λ + λ 2	.84
	"the quick brown fox	"the quick white fox	λ 2 -λ 3 + λ 4 -λ 6
	jumps over the lazy dog" crawls under the high dog"	+ λ 7 -λ 8 + λ 9 .45
	"me me me me..."	"me me me me..."	0	0

Table 2 .

 2 Position match matrix example, with discounting factor λ = .8.

Table 3 .

 3 Minimal and maximal distances between different types of papers depending on the discounting factor.

	type	discounting 0 .1 .2 .3 .4 .5 .6 .7 .8 .9 .95
	genuine / genuine	min	.23 .26 .30 .35 .40 .45 .52 .59 .68 .79 .86
		max	.55 .56 .57 .59 .61 .64 .67 .72 .78 .85 .90
	fake / fake	min	.26 .28 .31 .35 .39 .43 .49 .55 .63 .73 .81
		max	.38 .40 .43 .46 .49 .53 .58 .64 .71 .80 .86
	fake / genuine	min	.44 .46 .49 .52 .55 .59 .64 .70 .76 .84 .89
		max	.58 .60 .62 .64 .66 .68 .72 .76 .80 .87 .92

http://pdos.csail.mit.edu/scigen/

http://www.kongshoj.net/automogensen/

http://wordnet.princeton.edu/

Appendix

Proof of Theorem 1

Let φ be an optimal matching in D pm and let d pm (i, φ(i), 0) = 1 (if such i does not exist, then d 2 (A, B, 0) = 0 and we are done). Let w = a i . Assume that there is b j = w for which d pm (φ -1 (j), j) = 1, then we can define a new permutation φ by φ (i) = j and φ (φ -1 (j)) = φ(i) (and otherwise, values like φ), and φ is a better matching than φ, a contradiction.

Hence d pm (φ -1 (j), j) = 0 for all j such that b j = w. In other words, d pm (i, φ(i), 0) = 1 marks the fact that the word w = a i occurs one time more in A than in B. The same holds for all other indices i for which w = a i and d pm (i, φ(i), 0) = 1, so that

Similarly, if we let v = b φ(i) , then d pm (i, φ(i), 0) = 1 marks the fact that the word v occurs one time more in B than in A. Collecting these two, we see that

because φ was assumed optimal.


Uli Fahrenberg
email: ulrich.fahrenberg@inria.fr

Axel Legay

HOMOTOPY BISIMILARITY FOR HIGHER-DIMENSIONAL AUTOMATA

Keywords: 1.1, F.1.2, F.3.2, D.2.4 higher-dimensional automata, concurrency, homotopy, unfolding, higherdimensional trees

We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent events. For this, we use unfoldings of higher-dimensional automata into higher-dimensional trees. Using a notion of open maps in this category, we define homotopy bisimilarity. We show that homotopy bisimilarity is equivalent to a straightforward generalization of standard bisimilarity to higher dimensions, and that it is finer than split bisimilarity and incomparable with history-preserving bisimilarity.

Introduction

The dominant notion for behavioral equivalence of processes is bisimulation as introduced by Park [START_REF] David | Concurrency and automata on infinite sequences[END_REF] and Milner [START_REF] Milner | Communication and Concurrency[END_REF]. It is compelling because it enjoys good algebraic properties, admits several easy characterizations using modal logics, fixed points, or game theory, and generally has low computational complexity.

Bisimulation, or rather its underlying semantic model of transition systems, applies to a setting in which concurrency of actions is the same as non-deterministic interleaving; using CCS notation [START_REF] Milner | Communication and Concurrency[END_REF], a|b = a.b + b.a. For some applications however, a distinction between these two is necessary, which has led to development of so-called non-interleaving or truly concurrent models such as Petri nets [START_REF] Petri | Kommunikation mit Automaten[END_REF], event structures [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF], asynchronous transition systems [START_REF] Marek | Categories of asynchronous systems[END_REF][START_REF] Shields | Concurrent machines[END_REF] and others; see [START_REF] Winskel | Models for concurrency[END_REF] for a survey.

Higher-dimensional automata (or HDA) is another non-interleaving formalism for reasoning about behavior of concurrent systems. Introduced by Pratt [START_REF] Pratt | Modeling concurrency with geometry[END_REF] and van Glabbeek [START_REF] Van Glabbeek | Bisimulations for higher dimensional automata[END_REF] in 1991 for the purpose of a geometric interpretation to the theory of concurrency, it has since been shown by van Glabbeek [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF] that HDA provide a generalization (up to historypreserving bisimilarity) to "the main models of concurrency proposed in the literature" [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], including the ones mentioned above. Hence HDA are useful as a tool for comparing and relating different models, and also as a modeling formalism by themselves.

HDA are geometric in the sense that they are very similar to the simplicial complexes used in algebraic topology, and research on HDA has drawn on a lot of tools and methods from geometry and algebraic topology such as homotopy [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF][START_REF] Gaucher | Homotopy invariants of higher dimensional categories and concurrency in computer science[END_REF], homology [START_REF] Gaucher | About the globular homology of higher dimensional automata[END_REF][START_REF] Goubault | Homology of higher dimensional automata[END_REF], and model categories [START_REF] Gaucher | Homotopical interpretation of globular complex by multipointed d-space[END_REF][START_REF] Gaucher | Towards a homotopy theory of higher dimensional transition systems[END_REF], see also the survey [START_REF] Goubault | Geometry and concurrency: A user's guide[END_REF].

There are a number of popular notions of equivalence for HDA and other non-interleaving models, see [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF][START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF]. Split bisimilarity takes interleavings of beginning and ending actions into account; ST-bisimilarity additionally distinguishes between different occurrences of the same action; history-preserving bisimilarity takes entire computing histories into account; and hereditary history-preserving bisimilarity additionally distinguishes different possible futures of past computations.

We have in earlier work [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] introduced a new such equivalence, higher-dimensional bisimilarity. Contrary to the previously mentioned ones, this is not a relation between computations, but directly at the level of states, transitions etc. Using unfoldings of HDA, which geometrically are similar to universal coverings, we show in the present paper that this notion is equivalent to another one, homotopy bisimilarity, which compares homotopy classes of computations. Placing homotopy bisimulation on the spectrum of non-interleaving equivalences, we show that homotopy bisimilarity is finer than split bisimilarity and incomparable with history-preserving bisimilarity.

Our results imply decidability of homotopy bisimilarity for finite HDA. They also put homotopy bisimilarity firmly into the open-maps framework of [START_REF] Joyal | Bisimulation from open maps[END_REF] and tighten the connections between bisimilarity and weak topological fibrations [START_REF] Adámek | Weak factorization systems and topological functors[END_REF][START_REF] Kurz | Weak factorizations, fractions and homotopies[END_REF].

Outline. We start by reviewing the category HDA of higher-dimensional automata introduced in [START_REF] Goubault | Labelled cubical sets and asynchronous transition systems: an adjunction[END_REF] in Section 2. This is the category used in [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] as a framework to define composition, following [START_REF] Winskel | Models for concurrency[END_REF], and a notion of bisimilarity via open maps, following [START_REF] Joyal | Bisimulation from open maps[END_REF], for HDA. This latter construction, together with its notion of path category, we recall in Section 3.

Computations in HDA are modeled by cube paths, the higher-dimensional analogue of paths in transition systems. These come with a notion of homotopy which we introduce in Section 4. Based on homotopy classes of cube paths we can then define the construction at the heart of this paper, the unfolding of a HDA.

In Section 5 we introduce the category HDA h of higher-dimensional automata up to homotopy, based on unfoldings. We also show in this section that unfolding provides a coreflection between HDA and higher-dimensional trees, and between HDA-up-to-homotopy and higher-dimensional trees. In Section 6 we define homotopy bisimilarity via open maps in HDA h and show that this is the same as bisimilarity in HDA.

All these first sections deal with unlabeled higher-dimensional automata. In Section 7, we introduce labels using an arrow category construction and show that things can easily be transferred to the labeled setting. In Section 8 we compare homotopy bisimilarity to other equivalence notions for non-interleaving models.

Acknowledgements. The authors wish to thank Rob van Glabbeek for many useful discussions on the subject of this paper, and the organizers of SMC 2014 in Lyon for providing a forum for these discussions.

Higher-Dimensional Automata

As a formalism for concurrent behavior, HDA have the specific feature that they can express all higher-order dependencies between events in a concurrent system. Like for transition systems, they consist of states and transitions which are labeled with events. the square is filled in by a two-dimensional transition labeled ab, signifying independence of events a and b. On the right, a and b are not independent.

x δ 0 1 x δ 1 1 x δ 0 2 x δ 1 2 x δ 0 1 δ 0 2 x = δ 0 1 δ 0 1 x δ 0 1 δ 1 2 x = δ 1 1 δ 0 1 x δ 1 1 δ 0 2 x = δ 0 1 δ 1 1 x δ 1 1 δ 1 2 x = δ 1 1 δ 1 1 x
Figure 2: A 2-cube x with its four faces δ 0 1 x, δ 1 1 x, δ 0 2 x, δ 1 2 x and four corners. Now if two transitions from a state, with labels a and b for example, are independent, then this is expressed by the existence of a two-dimensional transition with label ab. Fig. 1 shows two examples; on the left, transitions a and b are independent, on the right, they can merely be executed in any order. Hence for HDA, as indeed for any formalism employing the so-called true concurrency paradigm, the algebraic law a|b = a.b + b.a does not hold; concurrency is not the same as interleaving.

The above considerations can equally be applied to sets of more than two events: if three events a, b, c are independent, then this is expressed using a three-dimensional transition labeled abc. Hence this is different from mutual pairwise independence (expressed by transitions ab, ac, bc), a distinction which cannot be made in formalisms such as asynchronous transition systems [START_REF] Marek | Categories of asynchronous systems[END_REF][START_REF] Shields | Concurrent machines[END_REF] or transition systems with independence [START_REF] Winskel | Models for concurrency[END_REF] which only consider binary independence relations.

An unlabeled HDA is essentially a pointed precubical set as defined below. For labeled HDA, one can pass to an arrow category; this is what we shall do in Section 7. Until then, we concentrate on the unlabeled case.

A precubical set is a graded set X = {X n } n∈AE together with mappings δ ν k : X n → X n-1 , k ∈ {1, . . . , n}, ν ∈ {0, 1}, satisfying the precubical identity

δ ν k δ µ ℓ = δ µ ℓ-1 δ ν k (k < ℓ) . (2.1)
The mappings δ ν k are called face maps, and elements of X n are called n-cubes. As above, we shall usually omit the extra subscript (n) in the face maps. Faces δ 0 k x of an element x ∈ X are to be thought of as lower faces, δ 1 k x as upper faces. The precubical identity expresses the fact that (n -1)-faces of an n-cube meet in common (n -2)-faces, see Fig. 2 for an example of a 2-cube and its faces.

We will always assume the sets X n to be disjoint. For an n-cube x ∈ X n , we denote by dim x = n its dimension.

Morphisms f : X → Y of precubical sets are graded mappings f = {f n : X n → Y n } n∈AE which commute with the face maps:

δ ν k • f n = f n-1 • δ ν k for all n ∈ AE, k ∈ {1, . . . , n}, ν ∈ {0, 1}
. This defines a category pCub of precubical sets and morphisms.

It can be shown [START_REF] Grandis | Cubical sets and their site[END_REF] that the category pCub is complete and cocomplete, with pointwise limits and colimits. In elementary terms this means that, for instance, the product

Z = X × Y of two precubical sets X, Y is given by Z n = X n × Y n and face maps δ ν k (x, y) = (δ ν k x, δ ν k y). Likewise, a precubical subset Y ⊆ X of X ∈ pCub is a precubical set Y for which Y n ⊆ X n for all n.
A pointed precubical set is a precubical set X with a specified 0-cube i ∈ X 0 , and a pointed morphism is one which respects the point. This defines a category which is isomorphic to the comma category * ↓ pCub, where * ∈ pCub is the precubical set with one 0-cube and no other n-cubes. Note that * is not terminal in pCub (instead, the terminal object is the somewhat unwieldy infinite-dimensional precubical set with one cube in every dimension).

Definition 2.1. The category of higher-dimensional automata is the comma category HDA = * ↓ pCub, with objects pointed precubical sets and morphisms commutative diagrams *

} } ④ ④ ④ ④ " " ❊ ❊ ❊ ❊ X f / / Y .
Hence a one-dimensional HDA is a transition system; indeed, the category of transition systems [START_REF] Winskel | Models for concurrency[END_REF] is isomorphic to the full subcategory of HDA spanned by the one-dimensional objects. Similarly one can show [START_REF] Goubault | Labelled cubical sets and asynchronous transition systems: an adjunction[END_REF] that the category of asynchronous transition systems is isomorphic to the full subcategory of HDA spanned by the (at most) two-dimensional objects. The category HDA as defined above was used in [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] to provide a categorical framework (in the spirit of [START_REF] Winskel | Models for concurrency[END_REF]) for parallel composition of HDA. In this article we also introduced a notion of higher-dimensional bisimilarity which we will review in the next section.

Path Objects, Open Maps and Bisimilarity

With the purpose of introducing bisimilarity via open maps in the sense of [START_REF] Joyal | Bisimulation from open maps[END_REF], we identify here a subcategory of HDA consisting of path objects and path-extending morphisms. We say that a precubical set X is a precubical path object if there is a (necessarily unique) sequence (x 1 , . . . , x m ) of elements in X such that x i = x j for i = j,

• for each x ∈ X there is j ∈ {1, . . . , m} for which

x = δ ν 1 k 1 • • • δ νp kp
x j for some indices ν 1 , . . . , ν p and a unique sequence k 1 < • • • < k p , and

• for each j = 1, . . . , m -1, there is k ∈ AE for which x j = δ 0 k x j+1 or x j+1 = δ 1 k x j . Note that precubical path objects are non-selflinked in the sense of [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF]. If X and Y are precubical path objects with representations (x 1 , . . . , x m ), (y 1 , . . . , y p ), then a morphism f : X → Y is called a cube path extension if x j = y j for all j = 1, . . . , m (hence m ≤ p). Definition 3.1. The category HDP of higher-dimensional paths is the subcategory of HDA which as objects has pointed precubical paths, and whose morphisms are generated by pointed cube path extensions and isomorphisms. Its computational interpretation is that a is executed first, then execution of b starts, and while b is running, c starts to execute. After this, b finishes, then c, and then execution of d is started. Note that the computation is partial, as d does not finish.

Example 3.2. HDP is not a full subcategory of HDA: If X and Y are the two higherdimensional paths depicted in Fig. 3, then none of the two mappings X → Y is a HDPmorphism.

A cube path in a precubical set X is a morphism P → X from a precubical path object P . In elementary terms, this is a sequence (x 1 , . . . , x m ) of elements of X such that for each j = 1, . . . , m-1, there is k ∈ AE for which x j = δ 0 k x j+1 (start of a new part of a computation) or x j+1 = δ 1 k x j (end of a computation part). Cube paths were introduced in [START_REF] Van Glabbeek | Bisimulations for higher dimensional automata[END_REF], where they are simply called paths. They are intended to model (partial) computations of HDA. We show an example of a cube path in Fig. 4.

A cube path in a HDA i : * → X is pointed if x 1 = i, hence if it is a pointed morphism P → X from a higher-dimensional path P . We will say that a cube path (x 1 , . . . , x m ) is from x 1 to x m , and that a cube x ∈ X in a HDA X is reachable if there is a pointed cube path to x in X.

Cube paths can be concatenated if the end of one is compatible with the beginning of the other: If ρ = (x 1 , . . . , x m ) and σ = (y 1 , . . . , y p ) are cube paths with y 1 = δ 1 k x m or x m = δ 0 k y 1 for some k, then their concatenation is the cube path ρ * σ = (x 1 , . . . , x m , y 1 , . . . , y p ). We say that ρ is a prefix of χ and write ρ ⊑ χ if there is a cube path ρ for which χ = ρ * σ.

Definition 3.3. A pointed morphism f : X → Y in HDA is an open map if it
has the right lifting property with respect to HDP, i.e. if it is the case that there is a lift r in any commutative diagram as below, for morphisms g :

P → Q ∈ HDP, p : P → X, q : Q → Y ∈ HDA: P p / / g X f Q q / / r ? ? Y HDA X, Y are hd-bisimilar if there is Z ∈ HDA and a span of open maps X ← Z → Y in HDA.
It follows straight from the definition that composites of open maps again are open. By the next lemma, morphisms are open precisely when they have a zig-zag property similar to the one of [START_REF] Joyal | Bisimulation from open maps[END_REF]. Lemma 3.4. For a morphism f : X → Y ∈ HDA, the following are equivalent:

(1) f is open;

(2) for any reachable x 1 ∈ X and any

y 2 ∈ Y with f (x 1 ) = δ 0 k y 2 for some k, there is x 2 ∈ X for which x 1 = δ 0 k x 2 and y 2 = f (x 2 ); (3) for any reachable x 1 ∈ X and any cube path (y 1 , . . . , y m ) in Y with y 1 = f (x 1 ),
there is a cube path (x 1 , . . . , x m ) in X for which y j = f (x j ) for all j = 1, . . . , m.

Proof. For the implication (1) =⇒ (2), let p : P → X be a pointed cube path with P represented by (p 1 , . . . , p m ) and p(p m ) = x 1 . Let p m+1 be a cube of dimension one higher than p m , set p m = δ 0 k p m+1 , and let Q be the higher-dimensional path represented by (p 1 , . . . , p m , p m+1 ). Let g : P → Q be the inclusion, and define q : Q → Y by q(p j ) = f (p(p j )) for j = 1, . . . , m and q(p m+1 ) = y 2 . We have a lift r : Q → X and can set x 2 = r(p m+1 ).

The implication (2) =⇒ (3) can be easily shown by induction. The case y m = δ 0 k y m+1 follows directly from (2), and the case

y m+1 = δ 1 k y m is clear by δ 1 k • f = f • δ 1 k .
To finish the proof, we show the implication (3) =⇒ (1). Let

P p / / g X f Q q / / Y
be a commutative diagram, with P represented by (p 1 , . . . , p m ). Up to isomorphism we can assume that Q is represented by (p 1 , . . . , p m , p m+1 , . . . , p t ) and that g is the inclusion. The cube p(p m ) is reachable in X, and (q(p m ), . . . , q(p t )) is a cube path in Y which starts in q(p m ) = f (p(p m )). Hence we have a cube path (x m , . . . , x t ) in X with x m = p(p m ) and q(p j ) = f (x j ) for all j = m, . . . , t, and we can define a lift r : Q → X by r(p j ) = p(p j ) for j = 1, . . . , m and r(p j ) = x j for j = m + 1, . . . , t.

Theorem 3.5. For HDA i : * → X, j : * → Y , the following are equivalent:

(1) X and Y are hd-bisimilar;

(2) there exists a precubical subset R ⊆ X × Y for which (i, j) ∈ R, and such that for all (x 1 , y 1 ) ∈ R,

• for any x 2 ∈ X for which x 1 = δ 0 k x 2 for some k, there exists y 2 ∈ Y for which (3) there exists a precubical subset R ⊆ X × Y for which (i, j) ∈ R, and such that for all (x 1 , y 1 ) ∈ R,

y 1 = δ 0 k y 2 and (x 2 , y 2 ) ∈ R, • for any y 2 ∈ Y for which y 1 = δ 0 k y 2 for some k, there exists x 2 ∈ X for which x 1 = δ 0 k x 2 and (x 2 , y 2 ) ∈ R;
• for any cube path (x 1 , . . . , x m ) in X, there exists a cube path (y 1 , . . . , y m ) in Y with (x p , y p ) ∈ R for all p = 1, . . . , m, • for any cube path (y 1 , . . . , y m ) in Y , there exists a cube path (x 1 , . . . , x m ) in X with (x p , y p ) ∈ R for all p = 1, . . . , m.

Proof. For the implication (1) =⇒ (2), let

X f ← -Z g -→ Y be a span of open maps and define R = {(x, y) ∈ X × Y | ∃z ∈ Z : x = f (z), y = g(z)}. Then (i, j) ∈ R

Homotopies and Unfoldings

In order to connect our notion of hd-bisimilarity with other common notions, we need to introduce in which cases different cube paths are equivalent due to independence of actions. Following [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], we model this equivalence by a combinatorial version of homotopy which is an extension of the equivalence defining Mazurkiewicz traces [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF].

We say that cube paths (x 1 , . . . , x m ), (y 1 , . . . , y m ) are adjacent if x 1 = y 1 , x m = y m , there is precisely one index p ∈ {1, . . . , m} at which x p = y p , and

• x p-1 = δ 0 k x p , x p = δ 0 ℓ x p+1 , y p-1 = δ 0
ℓ-1 y p , and y p = δ 0 k y p+1 for some k < ℓ, or vice versa,

• x p = δ 1 k x p-1 , x p+1 = δ 1 ℓ x p , y p = δ 1 ℓ-1 y p-1
, and y p+1 = δ 1 k y p for some k < ℓ, or vice versa, • x p = δ 0 k δ 1 ℓ y p , y p-1 = δ 0 k y p , and y p+1 = δ 1 ℓ y p for some k < ℓ, or vice versa, or • x p = δ 1 k δ 0 ℓ y p , y p-1 = δ 0 ℓ y p , and y p+1 = δ 1 k y p for some k < ℓ, or vice versa. Homotopy of cube paths is the reflexive, transitive closure of the adjacency relation. We denote homotopy of cube paths using the symbol ∼, and the homotopy class of a cube path (x 1 , . . . , x m ) is denoted [x 1 , . . . , x m ]. The intuition of adjacency is rather simple, even though the combinatorics may look complicated, see Fig. 5. Note that adjacencies come in two basic "flavors": the first two above in which the dimensions of x ℓ and y ℓ are the same, and the last two in which they differ by 2.

The following lemma shows that, not surprisingly, cube paths entirely contained in one cube are homotopic (provided that they share endpoints).

Lemma 4.1. Let x ∈ X n in a precubical set X and (k 1 , . . . , k n ), (ℓ 1 , . . . , ℓ n ) sequences of indices with k j , ℓ j ≤ j for all j = 1, . . . , n. Let x j = δ 0 k j • • • δ 0 kn x, y j = δ 0 ℓ j • • • δ 0 ℓn x.
Then the cube paths (x 1 , . . . , x n , x) ∼ (y 1 , . . . , y n , x).

Proof. (cf. [6, Ex. 2.15]). We can represent a cube path (x 1 , . . . , x n , x) as above by an element (p 1 , . . . , p n ) of the symmetric group S n by setting p n = k n and, working backwards, p j = ({1, . . . , n} \ {p j+1 , . . . , p n })[k j ], denoting by this the k j -largest element of the set in parentheses. This introduces a bijection between the set of cube paths from the lower left corner of x to x on the one hand, and elements of S n on the other hand, and under this bijection adjacencies of cube paths are transpositions in S n . These generate all of S n , hence all such cube paths are homotopic.

We extend concatenation and prefix to homotopy classes of cube paths by defining [x 1 , . . . , x m ] * [y 1 , . . . , y p ] = [x 1 , . . . , x m , y 1 , . . . , y p ] and saying that x ⊑ z, for homotopy classes x, z of cube paths, if there are (x 1 , . . . , x m ) ∈ x and (z 1 , . . . , z q ) ∈ z for which (x 1 , . . . , x m ) ⊑ (z 1 , . . . , z q ). It is easy to see that concatenation is well-defined, and that x ⊑ z if and only if there is a homotopy class ỹ for which z = x * ỹ.

Using homotopy classes of cube paths, we can now define the unfolding of a HDA. Unfoldings of HDA are similar to unfoldings of transition systems [START_REF] Winskel | Models for concurrency[END_REF] or Petri nets [START_REF] Hayman | The unfolding of general Petri nets[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF], but also to universal covering spaces in algebraic topology. The intention is that the unfolding of a HDA captures all its computations, up to homotopy.

We say that a HDA X is a higher-dimensional tree if it holds that for any x ∈ X, there is precisely one homotopy class of pointed cube paths to x. The full subcategory of HDA spanned by the higher-dimensional trees is denoted HDT. Note that any higher-dimensional path is a higher-dimensional tree; indeed there is an inclusion HDP ֒→ HDT. Definition 4.2. The unfolding of a HDA i : * → X consists of a HDA ĩ : * → X and a pointed projection morphism π X : X → X, which are defined as follows:

• Xn = [x 1 , . . . , x m ] | (x 1 , . . . , x m ) pointed cube path in X, x m ∈ X n ; ĩ = [i] • δ0 k [x 1 , . . . , x m ] = (y 1 , . . . , y p ) | y p = δ 0 k x m , (y 1 , . . . , y p , x m ) ∼ (x 1 , . . . , x m ) • δ1 k [x 1 , . . . , x m ] = [x 1 , . . . , x m , δ 1 k x m ] • π X [x 1 , . . . , x m ] = x m Proposition 4.3.
The unfolding ( X, π X ) of a HDA X is well-defined, and X is a higherdimensional tree. If X itself is a higher-dimensional tree, then the projection π X : X → X is an isomorphism.

Before proving the proposition, we need an auxiliary notion of fan-shaped cube path together with a technical lemma. Say that a cube path (x 1 , . . . , x m ) in a precubical set X, with x m ∈ X n , is fan-shaped if

x j ∈      X 0 for 1 ≤ j ≤ m -n odd, X 1 for 1 ≤ j ≤ m -n even, X n+j-m for m -n < j ≤ m .
Hence a fan-shaped cube path is a one-dimensional path up to the point where it needs to build up to hit the possibly high-dimensional end cube x m ; in computational terms, it is serialized.

Lemma 4.4. Any pointed cube path in a higher-dimensional automaton i : * → X is homotopic to a fan-shaped one.

Proof. Let us first introduce some notation: For any pointed cube path (x 1 , . . . , x m ), let n j = dim x j be the j-th component's dimension, and let T (x 1 , . . . , x m ) = n 1 + • • • + n m . An easy induction shows that jn j is odd for all j. Also, T (x 1 , . . . , x m ) ≥ 1 2 (n 2 m + m -1), with equality if and only if (x 1 , . . . , x m ) is fan-shaped.

Next we show that

n 1 + • • • + n m ≡ 1 2 (n 2 m + m -1) mod 2.
By oddity of jn j we have m j=1 n j -m j=1 j ≡ m mod 2, and also

1 2 (n 2 m + m -1) -m j=1 j = 1 2 (n 2 m -m 2 -1) ≡ m mod 2, hence the claim follows.
We can now finish the proof by showing how to convert a cube path (x 1 , . . . , x m ) with

T (x 1 , . . . , x m ) > 1 2 (n 2 m + m -1) into an adjacent cube path (x ′ 1 , . . . , x ′ m ) which has T (x ′ 1 , . . . , x ′ m ) = T (x 1 , . . . , x m )-2
, essentially by replacing one of its cubes, called x ℓ below, with another one of dimension n ℓ -2.

If (x 1 , . . . , x m ) is a cube path which is not fan-shaped, then there is an index ℓ ∈ {3, . . . , m -1} for which n ℓ ≥ 2, x ℓ-1 = δ 0 k 2 x ℓ for some k 2 , and x ℓ+1 = δ 1 k 3 x ℓ for some k 3 . Assuming ℓ to be the least such index, we must also have

x ℓ-2 = δ 0 k 1 x ℓ-1 for some k 1 . Now if k 2 < k 3 , then δ 0 k 2 x ℓ+1 = δ 0 k 2 δ 1 k 3 x ℓ = δ 1 k 3 -1 δ 0 k 2 x ℓ = δ 1 k 3 -1
x ℓ-1 by the precubical identity (2.1), hence we can let (x ′ 1 , . . . , x ′ m ) be the cube path with x ′ j = x j for j = ℓ and

x ′ ℓ = δ 0 k 2 x ℓ+1 . If k 2 > k 3 , then similarly δ 1 k 3 x ℓ-1 = δ 1 k 3 δ 0 k 2 x ℓ = δ 0 k 2 -1 δ 1 k 3 x ℓ = δ 0 k 2 -1
x ℓ+1 , and we can let x ′ j = x j for j = ℓ and x ′ ℓ = δ 1 k 3 x ℓ-1 . For the remaining case k 2 = k 3 , we replace x ℓ-1 by another cube of equal dimension first: If

k 1 < k 2 , then x ℓ-2 = δ 0 k 1 δ 0 k 2 x ℓ = δ 0 k 2 -1 δ 0 k 1 x ℓ , hence the cube path (x ′′ 1 , . . . , x ′′ m ) with x ′′ j = x j for j = ℓ -1 and x ′′ ℓ-1 = δ 0 k 1 x ℓ is adjacent to (x 1 , . . . , x m
), and T (x ′′ 1 , . . . , x ′′ m ) = T (x 1 , . . . , x m ). For this new cube path, we have

x ′′ ℓ-2 = δ 0 k 2 -1 x ′′ ℓ-1 , x ′′ ℓ-1 = δ 0 k 1 x ′′ ℓ , and x ′′ ℓ+1 = δ 1 k 3 x ′′ ℓ
, and as k 1 < k 3 , we can apply to the cube path (x ′′ 1 , . . . , x ′′ m ) the argument for the case k 2 < k 3 above.

If

k 1 ≥ k 2 , then x ℓ-2 = δ 0 k 1 δ 0 k 2 x ℓ = δ 0 k 2 δ 0 k 1 +1
x ℓ by another application of the precubical identity (2.1). Hence we can let x ′′ j = x j for j = ℓ -1 and Proof. Let (x 1 , . . . , xm ) be a pointed cube path in X, and write x j = π X xj for j = 1, . . . , m. Let (x 1 , . . . , x m , y 1 , . . . , y p ) be an extension in X and define ỹj = [x 1 , . . . , x m , y 1 , . . . , y j ] for j = 1, . . . , p. Then (x 1 , . . . , xm , ỹ1 , . . . , ỹp ) is the required extension in X, which is unique as X is a higher-dimensional tree.

x ′′ ℓ-1 = δ 0 k 1 +1 x ℓ . Then x ′′ ℓ-2 = δ 0 k 2 x ′′ ℓ-1 , x ′′ ℓ-1 = δ 0 k 1 +1 x ′′ ℓ ,
′ m-1 = δ 0 k x ′ m = δ 0 k x m , hence (x ′ 1 , . . . , x ′ m-1 ) ∈ δ0 k [x 1 , . . . , x m ].
Corollary 4.7. Projections are open, and any HDA is hd-bisimilar to its unfolding.

Higher-dimensional Automata up to Homotopy

Definition 5.1. The category of higher-dimensional automata up to homotopy HDA h has as objects HDA and as morphisms pointed precubical morphisms f : X → Ỹ of unfoldings.

Hence any morphism X → Y in HDA gives, by the unfolding functor, rise to a morphism X → Y in HDA h . The simple example in Fig. 6 shows that the converse is not the case. By restriction to higher-dimensional trees, we get a full subcategory HDT h ֒→ HDA h . Lemma 5.2. The natural projection isomorphisms π X : X → X for X ∈ HDT extend to an isomorphism of categories HDT h ∼ = HDT.

Proof. Using the projection isomorphisms, any morphism f : X → Y in HDT h can be "pulled down" to a morphism π Y • f • π -1 X : X → Y of HDT. Restricting the above isomorphism to the subcategory HDP of HDT allows us to identify a subcategory HDP h of HDT h isomorphic to HDP.

Analogously to the coreflection between transition systems and synchronization trees in [START_REF] Winskel | Models for concurrency[END_REF], we have a coreflection between higher-dimensional automata and higher-dimensional trees:

Proposition 5.3. The functor U : HDA → HDT given on objects by mapping X ∈ HDA to its unfolding X and on morphisms by mapping f : X → Y to f : X → Ỹ given by f [x 1 , . . . , x m ] = [f (x 1 ), . . . , f (x m )] is right adjoint to the forgetful functor HDT ֒→ HDA.

The counit morphisms are the projections π X : X → X.

Proof. First, U is indeed functorial, as f maps adjacent cube paths (x 1 , . . . , x m ) ∼ (y 1 , . . . , y m ) to cube paths (f x 1 , . . . , f x m ), (f y 1 , . . . , f y m ) which are identical or adjacent, hence f : X → Ỹ is well-defined.

To show adjointness, we need to see that any pointed morphism f : T → Y ∈ pCub from a higher-dimensional tree * → T to a higher-dimensional automaton * → Y factors uniquely as

f = π Y • g : T → Ỹ → Y . This amounts to filling-in the dotted arrow in the diagram Ỹ π Y / / Y T f O O π T / / T . f O O g _ _ By Proposition 4.3, π T has an inverse ψ T , hence g = f • ψ T is the unique filler.
Note that by Proposition 4.3, the unit morphisms are isomorphisms, hence the above adjunction is indeed a coreflection.

The following is the analogue of Proposition 5.3 for the homotopy categories, with a similar proof. Note however that here, U h is an isomorphism on morphisms.

Proposition 5.4. The forgetful functor HDT h ֒→ HDA h has a right adjoint U h given on objects by mapping X ∈ HDA h to its unfolding X and on morphisms by mapping f : X → Y to f : X → Ỹ . The counit morphisms are the projections π X : X → X.

The unit morphisms are again isomorphisms, hence the adjunction is a coreflection. Combining the functors of Propositions 5.3 and 5.4 with the isomorphism of Lemma 5.2, we have the following diagram of categories and coreflections. Note that the adjunctions do not compose.

HDA h U h / / ⊤ HDT h _ ? J h o o / / ∼ = HDT o o J / / ⊥ HDA U o o
The endofunctor J • U on HDA, which maps objects and morphisms to their unfoldings, splits into an adjunction between HDA and HDA h . Its left part is the "inclusion" HDA ֒→ HDA h which we already saw above. Proposition 5.5. There is a coreflection U 1 : HDA h ⇆ HDA : U 2 , with U 1 left and U 2 right adjoint given by U 1 (X) = X on objects, U 1 (f ) = f on morphisms, U 2 (X) = X on objects, and U 2 (f ) = f on morphisms. The counit morphisms are the projections π X : X → X.

Proof. We need to see that any precubical morphism f : X → Y factors uniquely as f = π Y • g : X → Ỹ → Y , but as X is a higher-dimensional tree, this is clear by the isomorphism π X : X → X in the diagram

Ỹ π Y / / Y Xf O O π X / / X . f O O g _ _ 6. Homotopy Bisimilarity Definition 6.1. A pointed morphism f : X → Y in HDA h is open if it
has the right lifting property with respect to HDP h , i.e. if it is the case that there is a lift r in any commutative diagram as below, for all morphism g : Proof. For the forward implication of the first claim, let

P → Q ∈ HDP h , p : P → X, q : Q → Y ∈ HDA h : P p / / g X f Q q / /
P p / / g Xf Q q / / Ỹ (6.1)
be a diagram in HDA with g : P → Q ∈ HDP; we need to find a lift Q → X.

Using the isomorphisms π P : P → P , π Q : Q → Q, we can extend this diagram to the left; note that g : P → Q is a morphism of HDP:

P ∼ = / / g p ′ & & P p / / g Xf Q ∼ = / / q ′ 8 8 Q q / / Ỹ (6.2)
Hence we have a diagram

P p ′ / / g X f Q q ′ / / Y
in HDA h , and as g : P → Q is a morphism of HDP h , we have a lift r : Q → X in HDA h . This gives a morphism r : Q → X ∈ HDA in Diagram (6.2), and by composition with the inverse of the isomorphism π

Q : Q → Q, a lift r ′ : Q → X ∈ HDA in Diagram (6.1).
For the back implication in the first claim, assume f : X → Ỹ ∈ HDA open and let

P p / / g X f Q q / / Y
be a diagram in HDA h with g : P → Q ∈ HDP h ; we need to find a lift Q → X. Transferring this diagram to the category HDA, we have

P p / / g Xf Q q / /
Ỹ and as g : P → Q is a morphism of HDP, we get the required lift.

To prove the second claim, let

P p / / h Xg Q q / /
Ỹ be a diagram in HDA with h : P → Q ∈ HDP. We can extend it using the projection morphisms:

P p / / h X π X / / g X g Q q / / Ỹ π Y / / Y
Because g is open in HDA, we hence have a lift

P p / / h X π X / / g X g Q q / / r 7 7 Ỹ π Y / / Y
and Lemma 4.6 then gives the required lift r ′ in the diagram 6 is open in HDA h , showing that X and Y are, as expected, homotopy bisimilar.

P p / / g Xπ X Q r / / r ′ ? ? X Example 6.3. The morphism f : X → Y in Fig.
We also need a lemma on prefixes in unfoldings.

Lemma 6.4. Let X be a HDA and x, z ∈ X. Then there is a cube path from x to z in X if and only if x ⊑ z.

Proof. For the forward implication, let (x, ỹ1 , . . . , ỹp ) be a cube path in X with ỹp = z, let (x 1 , . . . , x m ) ∈ x, and write y j = π X ỹj for all j. By Lemma 4.5, (x 1 , . . . , x m , y 1 , . . . , y p ) ∈ z.

For the other direction, let (x 1 , . . . , x m , y 1 , . . . , y p ) ∈ z such that (x 1 , . . . , x m ) ∈ x, and define ỹj = [x 1 , . . . , x m , y 1 , . . . , y j ] for all j. Then (x, ỹ1 , . . . , ỹp ) is the required cube path from x to z in X. Proposition 6.5. For HDA i : * → X, j : * → Y , the following are equivalent:

(1) X and Y are homotopy bisimilar;

(2) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all (x 1 , ỹ1 ) ∈ R,

• for any x2 ∈ X for which x1 = δ 0 k x2 for some k, there exists ỹ2 ∈ Ỹ for which ỹ1 = δ 0 k ỹ2 and (x 2 , ỹ2 ) ∈ R, • for any ỹ2 ∈ Ỹ for which ỹ1 = δ 0 k ỹ2 for some k, there exists x2 ∈ X for which x1 = δ 0 k x2 and (x 2 , ỹ2 ) ∈ R; (3) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all (x 1 , ỹ1 ) ∈ R,

• for any cube path (x 1 , . . . , xn ) in X, there exists a cube path (ỹ 1 , . . . , ỹn ) in Ỹ with (x p , ỹp ) ∈ R for all p = 1, . . . , n, • for any cube path (ỹ 1 , . . . , ỹn ) in Ỹ , there exists a cube path (x 1 , . . . , xn ) in X with (x p , ỹp ) ∈ R for all p = 1, . . . , n; (4) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all

(x 1 , ỹ1 ) ∈ R, • for any x2 ⊒ x1 in X, there exists ỹ2 ⊒ ỹ1 in Ỹ for which (x 2 , ỹ2 ) ∈ R, • for any ỹ2 ⊒ ỹ1 in Ỹ , there exists x2 ⊒ x1 in X for which (x 2 , ỹ2 ) ∈ R.
Again, the requirement that R be a precubical subset is equivalent to saying that whenever (x, ỹ) ∈ R, then also (δ ν k x, δ ν k ỹ) ∈ R for any k and ν ∈ {0, 1}. Proof. The implication (1) =⇒ (2) follows directly from Theorem 3.5, and (3) can be proven from (2) by induction. Equivalence of (3) and ( 4) is immediate from Lemma 6.4.

For the implication (3) =⇒ (1), we can use Theorem 3.5 to get a span

X f ← -R g -→ Ỹ
of open maps in HDA. Connecting these with the projection π R : R → R gives a span

X f •π R ← --- R g•π R ---→ Ỹ .
X f •π R ← ---R g•π R ---→ Y is a span of open maps in HDA h .
Theorem 6.6. HDA X, Y are homotopy bisimilar if and only if they are hd-bisimilar. andf and g are open by Lemma 6.2. Hence hd-bisimilarity implies homotopy bisimilarity.

Proof. A span of open maps X f ← -Z g -→ Y in HDA lifts to a span X f ← -Z g -→ Y in HDA h ,
For the other direction, let

X f ← -Z g -→ Y be a span of open maps in HDA h . In HDA, this is a span X f ← - Z g -→ Ỹ
, and composing with the projections yields X Proof. The condition in Thm. 3.5 [START_REF] Marek | Categories of asynchronous systems[END_REF] immediately gives rise to a fixed-point algorithm similar to the one used to decide standard bisimilarity, cf. [START_REF] Milner | Communication and Concurrency[END_REF].

π X •f ←--- Z π Y •g ---→ Y . By Lemma 6.
In order to be able to relate our notion of bisimilarity to other common notions in Section 8 below, we translate it to a relation between pointed cube paths, i.e. executions: Theorem 6.8. HDA i : * → X, j : * → Y are homotopy bisimilar if and only if there exists a relation R between pointed cube paths in X and pointed cube paths in Y for which ((i), (j)) ∈ R, and such that for all (ρ, σ) ∈ R with ρ = (x 1 , . . . , x m ) and σ = (y 1 , . . . , y p ),

• dim

x m = dim y p , • for all k = 1, . . . , dim x m , (ρ * δ 1 k x m , σ * δ 1 k y p ) ∈ R, • for all k = 1, . . . , dim x m , there exist ρ ′ ∈ δ0 k [ρ] and σ ′ ∈ δ0 k [σ] with (ρ ′ , σ ′ ) ∈ R, • for all ρ ′ ∼ ρ, there exists σ ′ ∼ σ with (ρ ′ , σ ′ ) ∈ R, • for all σ ′ ∼ σ, there exists ρ ′ ∼ ρ with (ρ ′ , σ ′ ) ∈ R, • for all ρ ′ ⊒ ρ, there exists σ ′ ⊒ σ with (ρ ′ , σ ′ ) ∈ R, • for all σ ′ ⊒ σ, there exists ρ ′ ⊒ ρ with (ρ ′ , σ ′ ) ∈ R.
Note how the last four conditions are reminiscent of the ones for history-preserving bisimilarity [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF].

Proof. For the "if" part of the theorem, assume that we have a relation R as in the theorem and define R ⊆

X × Ỹ by R = {([ρ], [σ]) | (ρ, σ) ∈ R}.
Then ( ĩ, j) ∈ R, and the first three conditions ensure that R is a precubical subset of X × Ỹ : By dim x m = dim y p , Rn ⊆ Xn × Ỹn for all n, the second condition implies that for all ([ρ], [σ]) ∈ R and all k, also δ1

k ([ρ], [σ]) = ([ρ * δ 1 k x m ], [σ * δ 1 k y m ]
) ∈ R, and using the third condition, also δ0

k ([ρ], [σ]) = ([ρ ′ ], [σ ′ ]) ∈ R. Now let (x 1 , ỹ1 ) ∈ R and x2 ⊒ x1 . We have ρ 1 ∈ x1 and σ 1 ∈ ỹ1 for which (ρ 1 , σ 1 ) ∈ R. Let ρ ′ 1 ∈ x1 and ρ 2 ∈ x2 such that ρ 2 ⊒ ρ ′ 1 , then ρ ′ 1 ∼ ρ 1 , hence we have σ ′ 1 ∼ σ 1 for which (ρ ′ 1 , σ ′ 1 ) ∈ R. By ρ 2 ⊒ ρ ′ 1 we also have σ 2 ⊒ σ ′ 1 for which (ρ 2 , σ 2 ) ∈ R, hence (x 2 = [ρ 2 ], [σ 2 ]
) ∈ R as was to be shown. The symmetric condition in Theorem 6.5(4) can be shown analogously.

For the other implication, let R ⊆ X× Ỹ be a precubical subset as in Theorem 6.5(4) and define a relation of pointed cube paths by

R = {(ρ, σ) | ([ρ], [σ]) ∈ R}. Then ((i), (j)) ∈ R. Let (ρ = (x 1 , . . . , x m ), σ = (y 1 , . . . , y p )) ∈ R, then dim x m = dim y p by Rn ⊆ Xn × Ỹn . Let k ∈ {1, . . . , dim x m }, then δ1 k ([ρ], [σ]) ∈ R and hence (ρ * δ 1 k x m , σ * δ 1 k y p ) ∈ R. Using δ0 k ([ρ], [σ]) ∈ R, we see that there must exist ρ ′ ∈ δ0 k [ρ] and σ ′ ∈ δ0 k [σ] with (ρ ′ , σ ′ ) ∈ R.
Now let (ρ, σ) ∈ R, then also (ρ ′ , σ ′ ) ∈ R for any ρ ′ ∼ ρ, σ ′ ∼ σ, showing the fourth and fifth conditions of the theorem. For the sixth one, let ρ ′ ⊒ ρ, then [ρ ′ ] ⊒ [ρ], hence we have ỹ2 ⊒ [σ] for which ([ρ ′ ], ỹ2 ) ∈ R. By definition of R we have (ρ ′ , σ ′ ) ∈ R for any σ ′ ∈ ỹ2 , and by ỹ2 ⊒ [σ], there is σ ′ ∈ ỹ2 for which σ ′ ⊒ σ, showing the sixth condition. The seventh condition is proved analogously.

Labels

For labeling HDA, we need a subcategory of pCub isomorphic to the category of sets and functions. Given a finite or countably infinite set S = {a 1 , a 2 , . . . }, we construct a precubical set !S = {!S n } by letting !S n = (a i 1 , . . . , a in ) | i k ≤ i k+1 for all k = 1, . . . , n -1 with face maps defined by δ ν k (a i 1 , . . . , a in ) = (a i 1 , . . . , a i k-1 , a i k+1 , . . . , a in ). Definition 7.1. The category of higher-dimensional tori HDO is the full subcategory of pCub generated by the objects !S.

As any object in HDO has precisely one 0-cube, the pointed category * ↓ HDO is isomorphic to HDO. Note that the objects in HDO indeed are tori: by definition, lower and upper boundaries of any n-cube agree, hence all n-cubes are loops. Lemma 7.2. HDO is isomorphic to the category of sets and functions.

Proof. A function f : S → T is lifted to !f : !S → !T by f (a 1 , . . . , a n ) = f (a 1 ), . . . , f (a n ) , where the elements on the right-hand side are re-sorted. This is easily seen to be a precubical mapping. The inverse direction follows from the fact that the objects in HDO are coskeletal on their 1-cubes, cf. [START_REF] Brown | On the algebra of cubes[END_REF][START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF]. Definition 7.3. The category of labeled higher-dimensional automata is the pointed arrow category LHDA = * ↓ pCub → HDO, with objects * → X → !S labeled pointed precubical sets and morphisms commutative diagrams

* | | ③ ③ ③ ③ ③ " " ❉ ❉ ❉ ❉ ❉ X f / / Y !S σ / / !T Remark 7.
4. If morphisms of labeled higher-dimensional automata are to model (functional) simulations, then one needs partial labeling morphisms σ. This can be achieved by introducing degeneracies for precubical sets, passing to the category Cub of cubical sets. One can then show that the full subcategory of Cub spanned by free cubical sets on higherdimensional tori is isomorphic to the category of finite sets and partial functions and define LHDA accordingly. This is indeed the approach taken in [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF][START_REF] Goubault | Labelled cubical sets and asynchronous transition systems: an adjunction[END_REF]. As we are only concerned with bisimilarity here, we do not need partial labeling morphisms.

We now fix a labeling set Σ; we will work in the category with morphisms *

| | ③ ③ ③ ③ ③ " " ❉ ❉ ❉ ❉ ❉ X f / / Y !Σ id / / !Σ Definition 7.5. A morphism (f, id) : ( * → X → !Σ) → ( * → Y → !Σ) in LHDA is open if its component f is open in HDA. Labeled HDA * → X → !Σ, * → Y → !Σ are hd-bisimilar if there is * → Z → !Σ ∈ LHDA and a span of open maps X ← Z → Y in LHDA.
The definitions of open maps and bisimilarity in HDA h can now easily be extended to the labeled case. Again, we will only need label-preserving morphisms.

Definition 7.6. The category of labeled higher-dimensional automata up to homotopy LHDA h has as objects labeled HDA * → X → !S and as morphisms pairs of precubical morphisms (f, σ)

: ( * → X → ! S) → ( * → Ỹ → ! T ) of unfoldings. Definition 7.7. A morphism (f, id) : ( * → X → !Σ) → ( * → Y → !Σ) in LHDA h is open if its component f is open in HDA h . Labeled HDA * → X → !Σ, * → Y → !Σ are homotopy bisimilar if there is a labeled HDA * → Z → !Σ and a span of open maps X ← Z → Y in LHDA h .
As a corollary, we see that * → X λ -→ !Σ, * → Y µ -→ !Σ are homotopy bisimilar if and only if there exists a precubical subset R ⊆ X × Ỹ like in Theorem 6.5 which respects homotopy classes of labels, i.e. for which λ(x) = μ(ỹ) for each (x, ỹ) ∈ R.

The proof of the next theorem is exactly the same as the one for Theorem 6.6.

Theorem 7.8. Labeled HDA X, Y are homotopy bisimilar if and only if they are hdbisimilar.

Relation to Other Equivalences

It remains to be seen how our homotopy bisimilarity relates to other notions of equivalence for concurrent systems.

For a labeled HDA * → X λ -→ !Σ, we extend λ to cube paths in X by λ(x 1 , . . . , x m ) = (λ(x 1 ), . . . , λ(x m )).

The following is a labeled version of Theorem 6.8.

Theorem 8.1. Labeled HDA * i -→ X λ -→ !Σ, * j -→ Y µ
-→ !Σ are homotopy bisimilar if and only if there exists a relation R between pointed cube paths in X and pointed cube paths in Y for which ((i), (j)) ∈ R, and such that for all (ρ, σ) ∈ R with ρ = (x 1 , . . . , x m ) and σ = (y 1 , . . . , y p ),

• for all k = 1, . . . , dim x m , (ρ * δ • for all σ ′ ⊒ σ, there exists ρ ′ ⊒ ρ with (ρ ′ , σ ′ ) ∈ R.

1 k x m , σ * δ 1 k y p ) ∈ R, • for all k = 1, . . . , dim x m , there exist ρ ′ ∈ δ0 k [ρ] and σ ′ ∈ δ0 k [σ] with (ρ ′ , σ ′ ) ∈ R, • λ(ρ) ∼ µ(σ), • for all ρ ′ ∼ ρ, there exists σ ′ ∼ σ with (ρ ′ , σ ′ ) ∈ R, • for all σ ′ ∼ σ, there exists ρ ′ ∼ ρ with (ρ ′ , σ ′ ) ∈ R, • for all ρ ′ ⊒ ρ, there exists σ ′ ⊒ σ with (ρ ′ , σ ′ ) ∈ R, x0 x1 x2 x3 x4 y1 a y2 b y3 b y4 y5 z x ′ 0 x ′ 1 x ′ 2 x ′ 4 y ′ 1 a y ′ 2 b y ′ 4 y ′ 5 z ′
Proof. For the "if" part of the theorem, assume that we have a relation R as in the theorem and define R ⊆ X × Ỹ by R = {([ρ], [σ]) | (ρ, σ) ∈ R}, as in the proof of Theorem 6.8. Let (ρ, σ) ∈ R and write ρ = (x 1 , . . . , x m ) and σ = (y 1 , . . . , y p ). By λ(ρ) ∼ µ(σ), also λ(x m ) = µ(y p ), which, as λ and µ are precubical mappings, implies that dim x m = dim y p . Thus R satisfies the conditions of Theorem 6.8, so we can infer that R ⊆ X × Ỹ is a precubical subset for which the conditions in Theorem 6.5(4) hold. Let (

[ρ], [σ]) ∈ R, then λ(ρ) ∼ µ(σ) entails λ[ρ] = μ[σ].
For the other direction, let R ⊆ X × Ỹ be a precubical subset as in Theorem 6. Theorem 8.2. Homotopy bisimilarity is not implied by ST-bisimilarity and incomparable with history-preserving bisimilarity.

Proof. This will follow from the examples below.

We finish this section by exposing several examples. The first two serve to position homotopy bisimilarity with regard to history-preserving bisimilarity, and the last shows a case in which homotopy bisimilarity distinguishes auto-concurrency in a way similar to ST-bisimilarity. Whether homotopy bisimilarity implies ST-bisimilarity, and whether it is implied by hereditary history-preserving (hhp) bisimilarity, is open.

Example 8.3. The two HDA in Fig. 7 are hd-bisimilar, as witnessed by the following precubical subset R ⊆ X × X ′ :

R 0 = {(x 0 , x ′ 0 ), (x 1 , x ′ 1 ), (x 2 , x ′ 2 ), (x 3 , x ′ 4 ), (x 4 , x ′ 4 )} R 1 = {(y 1 , y ′ 1 ), (y 2 , y ′ 2 ), (y 3 , y ′ 4 ), (y 4 , y ′ 4 ), (y 5 , y ′ 5 )} R 2 = {(z, z ′ )}
In [START_REF] Van Glabbeek | Petri net models for algebraic theories of concurrency[END_REF]Example 5.2.2] it is shown that the Petri-net translations of these HDA are STbisimilar, but not history-preserving bisimilar.

Example 8.4. We show by a bisimulation-game [START_REF] Stirling | Modal and temporal logics for processes[END_REF] type argument that the HDA in Fig. 8 are not hd-bisimilar. Note that in [START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF] it is shown that these systems are history-preserving bisimilar but not hhp-bisimilar. The starting configuration is (x 0 , x ′ 0 ), in which Player 1 (the spoiler) plays the x 0extension y 16 . Player 2 (the duplicator) must answer with either y ′ 2 or y ′ 10 . Playing y ′ 2 is losing, as Player 1 then can play the y ′ 2 -extension z ′ 1 , with label bc, which Player 2 cannot duplicate. Hence Player 2 must play y ′ 10 . Then Player 1 attacks by extending y 16 with z 5 , to which Player 2 can only answer z ′ 4 . Player 1 now retreats to the other lower boundary of z 5 , y 15 , to which Player 2 must answer y ′ 9 . But then Player 1 plays the y ′ 9 -extension z ′ 3 , with label ac, which Player 2 cannot duplicate. Hence the game is decided in favor of the spoiler.

Example 8.5. Again using a hd-bisimulation game, we show that the HDA in Fig. 9 are not hd-bisimilar. Note that according to [START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF], they are split bisimilar, but not ST-bisimilar.

From the initial configuration (x 0 , x ′ 0 ) of the game, the spoiler plays y 1 and then z 1 , leading to the configuration (z 1 , z ′ 1 ). Playing y 4 and then z 2 , the spoiler forces the configuration (z 2 , z ′ 2 ) and, playing y 8 and then z 4 , leads the game to the cc-labeled configuration (z 4 , z ′ 4 ). Here the spoiler plays y 12 , which the duplicator has to answer by the z ′ 4 -boundary in the same direction, hence y ′ 12 . But then the spoiler can play the cd-labeled z 5 , to which the duplicator has no answer.

Conclusion

We have introduced a notion of homotopy bisimilarity for HDA which can be characterized as an equivalence relation between homotopy classes of computations, or equivalently by a zig-zag relation between cubes in all dimensions. Aside from implying decidability of homotopy bisimilarity for finite HDA, and together with the results of [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], this confirms that HDA is a useful formalism for concurrency: not only does it generalize the main models for concurrency which people have been working with, but it also is remarkably simple and natural.

One major question which remains is how precisely homotopy bisimilarity fits into the spectrum of equivalence notions for non-interleaving models. We have shown that it is finer than split bisimilarity and incomparable with history-preserving bisimilarity, but we miss to see whether homotopy bisimilarity implies ST-bisimilarity and whether it is implied by hhp-bisimilarity.

With regard to the geometric interpretation of HDA as directed topological spaces, there are two open questions related to the work laid out in the paper: In [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] we show that morphisms in HDA are open if and only if their geometric realizations lift pointed directed paths. This shows that there are some connections to weak factorization systems [START_REF] Adámek | Weak factorization systems and topological functors[END_REF] here which should be explored; see [START_REF] Kurz | Weak factorizations, fractions and homotopies[END_REF] for a related approach.

In [START_REF] Fahrenberg | Higher-Dimensional Automata from a Topological Viewpoint[END_REF] we relate homotopy of cube paths to directed homotopy of directed paths in the geometric realization. Based on this, one should be able to prove that the geometric realization of the unfolding of a HDA is the same as the universal directed covering [START_REF] Fajstrup | A convenient category for directed homotopy[END_REF] of its geometric realization.

Figure 1 :

 1 Figure 1: HDA for the CCS expressions a|b (left) and a.b + b.a (right). In the left HDA, the square is filled in by a two-dimensional transition labeled ab, signifying independence of events a and b. On the right, a and b are not independent.

Figure 3 :

 3 Figure 3: Two higher-dimensional paths with no HDP-morphism between them.

Figure 4 :

 4 Figure 4: Graphical representation of the two-dimensional cube path (i, a, x, b, bc, c, z, d).Its computational interpretation is that a is executed first, then execution of b starts, and while b is running, c starts to execute. After this, b finishes, then c, and then execution of d is started. Note that the computation is partial, as d does not finish.

Figure 5 :

 5 Figure 5: Graphical representation of the cube path homotopy (i, a, x, b, bc, c, z, d) ∼ (i, a, x, c, bc, c, z, d) ∼ (i, a, x, c, bc, b, z, d) ∼ (i, a, x, c, y, b, z, d).

1 ← -R π 2 -

 12 because f and g are pointed morphisms, and the other properties follow by Lemma 3.4. The implication (2) =⇒ (3) can be shown by a simple induction, and for the implication (3) =⇒ (1), the projections give a span X π → Y and are open by Lemma 3.4.

Figure 6 :

 6 Figure 6: Two simple one-dimensional HDA as objects of HDA and HDA h . In HDA there is no morphism X → Y , in HDA h there is precisely one morphism f : X → Y .

Y

  HDA X, Y are homotopy bisimilar if there is Z ∈ HDA h and a span of open maps X ← Z → Y in HDA h . The connections between open maps in HDA h and open maps in HDA are as follows. Lemma 6.2. A morphism f : X → Y in HDA h is open if and only if f : X → Ỹ is open as a morphism of HDA. If g : X → Y is open in HDA, then so is g : X → Ỹ .

  2 and Corollary 4.7, both π x • f and π Y • g are open in HDA. Corollary 6.7. Homotopy bisimilarity is decidable for finite HDA.

Figure 7 :

 7 Figure 7: Two HDA pertaining to Example 8.3.

  5(4) which respects labels. Define a relation of pointed cube paths by R = {(ρ, σ) | ([ρ], [σ]) ∈ R}, then R satisfies the conditions of Theorem 6.8. Let (ρ, σ) ∈ R, then ([ρ], [σ]) ∈ R implies λ[ρ] = μ[σ], hence λ(ρ) ∼ µ(σ).

4 Figure 8 :

 48 Figure 8: Two HDA pertaining to Example 8.4.

11 Figure 9 :

 119 Figure 9: Two HDA pertaining to Example 8.5.

  and x ′′ ℓ+1 = δ 1 k 3 x ′′ ℓ , and as k 1 + 1 > k 3 , we can apply the argument for the case k 2 > k 3 above.Proof of Theorem 4.3. It is clear that the structure maps δ1k are well-defined. For showing that also the mappings δ0 k are well-defined, we note first that δ0 k [x 1 , . . . , x m ] is independent of the representative chosen for [x 1 , . . . , x m ]: If (x ′ 1 , . . . , x ′ m ) ∼ (x 1 , . . . , x m ), then (y 1 , . . . , y p ) ∈ δ0

k [x ′ 1 , . . . , x ′ m ] if and only if y p = δ 0 k x ′ m = δ 0 k x m and (y 1 , . . . , y p , x ′ m ) = (y 1 , . . . , y p , x m ) ∼ (x ′ 1 , . . . , x ′ m ) ∼ (x 1 , . . . , x m ), if and only if (y 1 , . . . , y p ) ∈ δ0 k [x 1 , . . . , x m ]. We are left with showing that δ0 k [x 1 , . . . , x m ] is non-empty. By Lemma 4.4 there is a fan-shaped cube path (x ′ 1 , . . . , x ′ m ) ∈ [x 1 , . . . , x m ], and by Lemma 4.1 we can assume that x

  By Corollary 4.7, the maps in the span are open in HDA, hence by Lemma 6.2,

We need to show the precubical identity δν

δν k for k < ℓ and ν, µ ∈ {0, 1}. For ν = µ = 1 this is clear, and for ν = µ = 0 one sees that (y 1 , . . . , y p ) ∈ δ0 k δ0

ℓ [x 1 , . . . , x m ] if and only if y p = δ 0 k δ 0 ℓ x m = δ 0 ℓ-1 δ 0 k x m and (x 1 , . . . , x m ) ∼ (y 1 , . . . , y p , δ 0 ℓ x m , x m ) ∼ (y 1 , . . . , y p , δ 0 k x m , x m ), by adjacency. The cases ν = 1, µ = 0 and ν = 0, µ = 1 are similar to each other, so we only show the former.

The proof that * → X is a higher-dimensional tree follows from Lemma 4.5 below: Let (x 1 , . . . , xm ), (ỹ 1 , . . . , ỹm ) be pointed cube paths in X with xm = ỹm , then we need to prove that (x 1 , . . . , xm ) ∼ (ỹ 1 , . . . , ỹm ). Let x j = π X xj , y j = π X ỹj for j = 1, . . . , m be the projections, then (x 1 , . . . , x m ), (y 1 , . . . , y m ) are pointed cube paths in X. By Lemma 4.5, (x 1 , . . . , x j ) ∈ xj and (y 1 , . . . , y j ) ∈ ỹj for all j = 1, . . . , m.

By xm = ỹm , we know that (x 1 , . . . , x m ) ∼ (y 1 , . . . , y m ). Let (x 1 , . . . , x m ) = (z for all j = α. Then (z ℓ 1 , . . . , z ℓ j ) = (z ℓ+1 1 , . . . , z ℓ+1 j ) for j < α and (z ℓ 1 , . . . , z ℓ j ) ∼ (z ℓ+1 1 , . . . , z ℓ+1 j ) for j > α, hence there is an adjacency (z ℓ 1 , . . . , zℓ m ) ∼ (z ℓ+1 1 , . . . , zℓ+1 m ). For the last claim of the proposition, if X itself is a higher-dimensional tree, then an inverse to π X is given by mapping x ∈ X to the unique equivalence class [x 1 , . . . , x m ] ∈ X of any pointed cube path (x 1 , . . . , x m ) in X with x m = x. Lemma 4.5. If X is a higher-dimensional automaton and (x 1 , . . . , xm ) is a pointed cube path in X, then (π X x1 , . . . , π X xj ) ∈ xj for all j = 1, . . . , m.

Proof. Let x j = π X xj , for j = 1, . . . , m, then (x 1 , . . . , x m ) is a pointed cube path in X. We show the claim by induction: We have x1 = ĩ = [i] = [x 1 ], so assume that (x 1 , . . . , x j ) ∈ xj for some j ∈ {1, . . . , m -1}. If xj+1 = δ1 k xj for some k, then x j+1 = δ 1 k x j , and (x 1 , . . . , x j+1 ) ∈ xj+1 by definition of δ1 k . Similarly, if xj = δ0 k xj+1 for some k, then x j = δ 0 k x j+1 , and (x 1 , . . . , x j+1 ) ∈ xj+1 by definition of δ0 k . Lemma 4.6. For any HDA X there is a unique lift r in any commutative diagram as below, for morphisms g : P → Q ∈ HDP, p : P → X, q : Q → X ∈ HDA: