BRICS RS-99-19 Jurdziński & Nielsen: Hereditary History Preserving Bisimilarity is Undecidable BRICS

Basic Research in Computer Science

Hereditary History Preserving Bisimilarity is Undecidable

Marcin Jurdziński Mogens Nielsen BRICS Report Series RS-99-19 ISSN 0909-0878 June 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Marcin Jurdziński & Mogens Nielsen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/19/

Hereditary History Preserving Bisimilarity Is Undecidable

Marcin Jurdziński^{∗} Mogens Nielsen^{∗} BRICS^{†} Department of Computer Science University of Aarhus

June 1999

Abstract

We show undecidability of hereditary history preserving bisimilarity for finite asynchronous transition systems by a reduction from the halting problem of deterministic 2-counter machines. To make the proof more transparent we introduce an intermediate problem of checking domino bisimilarity for origin constrained tiling systems. First we reduce the halting problem of deterministic 2-counter machines to origin constrained domino bisimilarity. Then we show how to model domino bisimulations as hereditary history preserving bisimulations for finite asynchronous transitions systems. We also argue that the undecidability result holds for finite 1-safe Petri nets, which can be seen as a proper subclass of finite asynchronous transition systems.

1 Hereditary history preserving bisimilarity

Definition 1 (Labelled asynchronous transition system) A labelled asynchronous transition system is a tuple A = (S, s^{ini}, E, →, L, λ, I), where S is its set of states, s^{ini} ∈ S is the initial state, E is the set of events, → ⊆ S × E × S is the set of transitions, L is the set of labels, and λ : E → L is the labelling function, and I ⊆ E^{2} is the independence relation which is irreflexive and symmetric. We often write s →^{e} s′, instead of (s, e, s′) ∈ →. Moreover, the following conditions have to be satisfied:

1. if s →^{e} s′, and s →^{e} s′′, then s′ = s′′,

∗Address: BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, 8000 Aarhus C, Denmark. Emails: {mju,mn}@brics.dk.

† Basic Research in Computer Science, Centre of the Danish National Research Foundation.

2. if (e, e′) ∈ I, s →^{e} s′, and s′ →^{e′} t, then s →^{e′} s′′, and s′′ →^{e} t for some

s′′ ∈ S.

An asynchronous transition system is coherent if it satisfies one further condition:

3. if (e, e′) ∈ I, s →^{e} s′, and s →^{e′} s′′, then s′ →^{e′} t, and s′′ →^{e} t for some t ∈ S.

[Definition 1] □

Asynchronous transition systems were introduced independently by Bednarczyk [Bed88], and Shields [Shi85]. Winskel and Nielsen [WN95, NW96] give a thorough survey and establish formal relationships between asynchronous transition systems and other models for concurrency, such as Petri nets, and event structures.

The definition of an asynchronous transition system may seem to be quite liberal, in the sense that it requires the transition system to satisfy very few properties related to its independence relation. For example, labelled asynchronous transition systems arising from finite labelled 1-safe Petri nets form a proper subclass of the class of all finite coherent asynchronous transitions systems. We want to stress, however, that we have chosen this liberal definition only for technical convenience. In fact, as we show in section 4, the proof of our undecidability result goes through even for finite labelled 1-safe Petri nets.

Let A = (S, s^{ini}, E, →, L, λ, I) be a labelled asynchronous transition system. A sequence of events \overline{e} = ⟨e_{1}, e_{2}, …, e_{n}⟩ ∈ E^{n} is a run of A if there are states s_{1}, s_{2}, …, s_{n+1} ∈ S, such that s_{1} = s^{ini}, and for all i ∈ [n] we have s_{i} →^{e_{i}} s_{i+1}. We denote the set of runs of A by Run(A). We say that k ∈ [n] is most recent in \overline{e}, and we denote it by k ∈ MR(\overline{e}), if and only if (e_{k}, e_{ℓ}) ∈ I for all k < ℓ ≤ n. Note that if k ∈ MR(\overline{e}) then \overline{e} ⍉ k = ⟨e_{1}, …, e_{k−1}, e_{k+1}, …, e_{n}⟩ ∈ Run(A).

Definition 2 (Hereditary history preserving bisimulation) Let A_{i} = (S_{i}, s_{i}, E_{i}, →_{i}, L, λ_{i}, I_{i}) for i ∈ {1, 2} be labelled asynchronous transition systems. A relation B ⊆ Run(A_{1}) × Run(A_{2}) is a hereditary history preserving (hhp-) bisimulation relating A_{1} and A_{2} if the following conditions are satisfied:

1. (ε, ε) ∈ B,

and if (\overline{e_{1}}, \overline{e_{2}}) ∈ B then:

2. for all e_{1} ∈ E_{1}, if \overline{e_{1}} · e_{1} ∈ Run(A_{1}), then there exists e_{2} ∈ E_{2}, such that \overline{e_{2}} · e_{2} ∈ Run(A_{2}), and λ_{1}(e_{1}) = λ_{2}(e_{2}), and (\overline{e_{1}} · e_{1}, \overline{e_{2}} · e_{2}) ∈ B,

3. for all e_{2} ∈ E_{2}, if \overline{e_{2}} · e_{2} ∈ Run(A_{2}), then there exists e_{1} ∈ E_{1}, such that \overline{e_{1}} · e_{1} ∈ Run(A_{1}), and λ_{1}(e_{1}) = λ_{2}(e_{2}), and (\overline{e_{1}} · e_{1}, \overline{e_{2}} · e_{2}) ∈ B, 4. k ∈ MR(\overline{e_{1}}), if and only if k ∈ MR(\overline{e_{2}}),

5. if k ∈ MR(\overline{e_{1}}) = MR(\overline{e_{2}}), then (\overline{e_{1}} ⍉ k, \overline{e_{2}} ⍉ k) ∈ B.

A relation B ⊆ Run(A_{1}) × Run(A_{2}) is a history preserving (hp-) bisimulation if it satisfies conditions 1.–4. [Definition 2] □

We say that two asynchronous transition systems A_{1}, and A_{2} are hereditary history preserving (hhp-) bisimilar, if there is a hhp-bisimulation relating them; they are history preserving (hp-) bisimilar, if there is a history preserving bisimulation relating them.

Remark 1 Notice that for standard labelled transition systems, i.e., asynchronous transition systems without the independence relation, (h)hp-bisimi-larity coincides with the standard bisimilarity. If the independence relation is empty then only the latest event is most recent, so conditions 4. and 5. are redundant. [Remark 1] ◇

Remark 2 Hhp- and hp-bisimilarities are so called non-interleaving notions of equivalence for concurrent programs. They are different from the standard interleaving bisimulation in that they relate behaviours of concurrent programs viewed as partial orders of events ordered by causality relation, rather than as interleavings, i.e., sequences of events. We sketch below the standard partial order semantics for asynchronous transition systems, and we explain how notions of (h)hp-bisimilarity arise naturally in this context. The rest of the paper does not rely on any of the concepts discussed in this remark, so it can be safely omited in first reading.

Let A = (S, s^{ini}, E, →, L, λ, I) be a labelled asynchronous transition system. For every run \overline{e} ∈ E^{n} of A the independence relation induces an Elabelled partial order π(\overline{e}) = ([n], ⊴, ε), where ε : [n] → E is the labelling function. For all i ∈ [n] we set ε(i) = e_{i}. For i, j ∈ [n] we define i ⋖ j to hold, if i ≤ j, and (e_{i}, e_{j}) ∉ I. We get ⊴ as the transitive closure of ⋖. For \overline{e}, \overline{e′} ∈ Run(A) we define \overline{e} ≅ \overline{e′} to hold, if the corresponding labelled partial orders π(\overline{e}) and π(\overline{e′}) are isomorphic. This is clearly an equivalence relation.

The set of partial order runs PORun(A) of A is the set Run(A)/≅, i.e., isomorphism classes of E-labelled partial orders corresponding to runs of A. Let τ = (|τ|, ⊴, ε) be a partial order run of A, where ε : |τ| → E is the labelling function. A partial order behaviour corresponding to run τ is the L-labelled partial order λ(τ) = (|τ|, ⊴, λ ∘ ε).

A non-interleaving notion of behavioural equivalence for concurrent programs should respect the partial order semantics, i.e., it should relate isomorphic partial order behaviours.

Before we give an alternative definition of hereditary history preserving bisimulation we introduce some notations. If τ ∈ PORun(A), and \overline{e} ∈ τ, and \overline{e} · e ∈ Run(A), for some e ∈ E, then we write τ ⊕ e for [\overline{e} · e]≅ ∈ PORun(A); otherwise τ ⊕ e is undefined. Similarly, if \overline{e} ∈ τ, and \overline{e} = \overline{e′} · e, for some \overline{e′} ∈ Run(A), and e ∈ E, then we write τ ⊖ e for [\overline{e′}]≅ ∈ PORun(A); otherwise τ ⊖ e is undefined. By Iso(L) we denote the set of isomorphisms of L-labelled partial orders. By POBeh(A_{1}, A_{2}) we denote the set of triples (τ_{1}, Ξ, τ_{2}) ∈ PORun(A_{1})×Iso(L)×PORun(A_{2}), such that Ξ : |τ_{1}| → |τ_{2}| is an isomorphism of L-labelled partial orders λ_{1}(τ_{1}) and λ_{2}(τ_{2}), i.e., an isomorphism of partial order behaviours corresponding to partial order runs τ_{1} and τ_{2}.

Let (τ_{1}, Ξ, τ_{2}) ∈ POBeh(A_{1}, A_{2}), and let τ_{i}⊕e_{i} ∈ PORun(A_{i}) be defined for some e_{i} ∈ E_{i} for i = 1, 2. If the unique extension Ξ′ : |τ_{1} ⊕ e_{1}| → |τ_{2} ⊕ e_{2}| of Ξ (i.e., Ξ′ ⊃ Ξ) is an isomorphism of the L-labelled partial orders λ_{1}(τ_{1}⊕e_{1}), and λ_{2}(τ_{2}⊕e_{2}), then by (τ_{1}, Ξ, τ_{2})⊕(e_{1}, e_{2}) we denote the triple (τ_{1}⊕e_{1}, Ξ′, τ_{2}⊕e_{2}) ∈ POBeh(A_{1}, A_{2}). Otherwise (τ_{1}, Ξ, τ_{2}) ⊕ (e_{1}, e_{2}) is undefined.

Similarly, if τ_{i} ⊖e_{i} ∈ PORun(A_{i}) are defined for some e_{i} ∈ E_{i}, and i = 1, 2, and moreover the restriction Ξ′ of Ξ to |τ_{1}⊖e_{1}| is an isomorphism of L-labelled partial orders λ(τ_{1}⊖e_{1}), and λ_{2}(τ_{2}⊖e_{2}), then by (τ_{1}, Ξ, τ_{2})⊖(e_{1}, e_{2}) we denote the triple (τ_{1} ⊖ e_{1}, Ξ′, τ_{2} ⊖ e_{2}) ∈ POBeh(A_{1}, A_{2}); otherwise (τ_{1}, Ξ, τ_{2}) ⊖ (e_{1}, e_{2}) is undefined.

Now we are ready to give an alternative definition of hereditary history preserving bisimulation.

Definition 2’ (Hereditary history preserving bisimulation) Let A_{i} = (S_{i}, s_{i}, E_{i}, →_{i}, L, λ_{i}, I_{i}) for i ∈ {1, 2} be labelled asynchronous transition systems. A relation B ⊆ POBeh(A_{1}, A_{2}) is a hereditary history preserving (hhp-) bisimulation relating A_{1} and A_{2} if the following conditions are satisfied:

1. (∅, ∅, ∅) ∈ B,

and if (τ_{1}, Ξ, τ_{2}) ∈ B then:

2. for all e_{1} ∈ E_{1}, if τ_{1} ⊕ e_{1} is defined, then there is e_{2} ∈ E_{2}, such that (τ_{1}, Ξ, τ_{2}) ⊕ (e_{1}, e_{2}) is defined, and (τ_{1}, Ξ, τ_{2}) ⊕ (e_{1}, e_{2}) ∈ B,

3. for all e_{2} ∈ E_{2}, if τ_{2} ⊕ e_{2} is defined, then there is e_{1} ∈ E_{1}, such that (τ_{1}, Ξ, τ_{2}) ⊕ (e_{1}, e_{2}) is defined, and (τ_{1}, Ξ, τ_{2}) ⊕ (e_{1}, e_{2}) ∈ B,

4. for all e_{i} ∈ E_{i}, and i = 1, 2, if (τ_{1}, Ξ, τ_{2}) ⊖ (e_{1}, e_{2}) is defined, then (τ_{1}, Ξ, τ_{2}) ⊖ (e_{1}, e_{2}) ∈ B.

A relation B ⊆ POBeh(A_{1}, A_{2}) is a hp-bisimulation relating A_{1} and A_{2} if it satisfies conditions 1.–3. [Definition 2’] □

It can be shown that notions of bisimilarity induced by Definitions 2 and 2’ are equivalent [NC95]; we have decided to make Definition 2 the primary one here, since it is technically simpler and more intuitive. [Remark 2] ◇

Hp-bisimilarity has been introduced by many authors, among others Rabinovich and Trakhtenbrot [RT88], and van Glabbeek and Goltz [vGG89]. Hhp-bisimilarity has been introduced by Bednarczyk [Bed91], and discovered independently by Joyal et al. [JNW96], as the open map bisimulation for observations being labelled partial orders.

Nielsen and Clausen [NC95] have established game and logic characterizations of hhp-bisimilarity. An hhp-bisimulation game is played by two players Spoiler and Duplicator on the graphs of (partial order) runs of asynchronous transition systems. Spoiler wants to show that the two asynchronous transition systems are not hhp-bisimilar. Duplicator has a winning strategy if and only if the two asynchronous transition systems are hhp-bisimilar, and an hhpbisimulation is in fact a winning strategy for Duplicator. Hhp-bisimulation games can be seen as Ehrenfeucht-Fraïssé games for a modal logic with a backwards modality interpreted over the graphs of partial order runs of asynchronous transition systems, i.e., there is a hhp-bisimulation relating two asynchronous transition systems, if and only if they are indistinguishable by formulas of the logic.

History preserving bisimilarity has been shown to be decidable for 1-safe Petri nets by Vogler [Vog91], and to be DEXP-complete by Jategaonkar, and Mayer [JM96]. Decidability of hereditary history preserving bisimulation for 1-safe Petri nets has remained open instead [NW96, FH99]. Fröschle and Hildebrandt [FH99] have discovered an infinite hierarchy of bisimilarity notions refining hp-bisimilarity, and coarser than hhp-bisimilarity; hhp-bisimilarity is the intersection of all the bisimilarities in the hierarchy. They have shown all the bisimilarities in the hierarchy to be decidable for 1-safe Petri nets. Fröschle [Frö99] has shown hhp-bisimilarity to be decidable for BPP-processes.

The main result of this paper is the following theorem proved in section 3.

Theorem 3 (Undecidability of hhp-bisimilarity) Hhp-bisimilarity for finite labelled asynchronous transition systems is undecidable.

2 Domino bisimilarity is undecidable

2.1 Domino bisimilarity

Definition 4 (Origin constrained tiling system) An origin constrained tiling system T = (D, D^{ori}, (H, H^{0}), (V, V^{0}), L, λ) consists of a set D of dominoes, its subset D^{ori} ⊆ D called the origin constraint, two horizontal compatibility relations H, H^{0} ⊆ D^{2}, two vertical compatibility relations V, V^{0} ⊆ D^{2}, a set L of labels, and a labelling function λ : D → L.

[Definition 4] □

A configuration of T is a triple (d, x, y) ∈ D × ℕ × ℕ, such that if x = y = 0 then d ∈ D^{ori}. In other words, in the “origin” position (x, y) = (0, 0) of the non-negative integer grid only dominoes from the origin constraint D^{ori} are allowed.

Let (d, x, y), and (d′, x′, y′) be configurations of T such that |x′ − x| + |y′ − y| = 1, i.e., the positions (x, y), and (x′, y′) are neighbours in the non-negative integer grid. Without loss of generality we may assume that x + y < x′ + y′. We say that configurations (d, x, y), and (d′, x′, y′) are compatible if either of the two conditions below holds:

• x′ = x, and y′ = y + 1, and if y = 0, then (d, d′) ∈ V^{0}, and if y > 0, then (d, d′) ∈ V, or

• x′ = x + 1, and y′ = y, and if x = 0, then (d, d′) ∈ H^{0}, and if x > 0, then (d, d′) ∈ H.

Definition 5 (Domino bisimulation) Let T_{i} = (D_{i}, D_{i}^{ori}, (H_{i}, H_{i}^{0}), (V_{i}, V_{i}^{0}), L_{i}, λ_{i}) for i ∈ {1, 2} be origin constrained tiling systems. A relation B ⊆ D_{1} × D_{2} × ℕ × ℕ is a domino bisimulation relating T_{1} and T_{2}, if the following conditions are satisfied for all i ∈ {1, 2}:

1. for all d_{i} ∈ D_{i}^{ori}, there exists d_{3−i} ∈ D_{3−i}^{ori}, such that λ_{1}(d_{1}) = λ_{2}(d_{2}), and (d_{1}, d_{2}, 0, 0) ∈ B,

2. for all x, y ∈ ℕ, such that (x, y) ≠ (0, 0), and d_{i} ∈ D_{i}, there exists d_{3−i} ∈ D_{3−i}, such that λ_{1}(d_{1}) = λ_{2}(d_{2}), and (d_{1}, d_{2}, x, y) ∈ B,

3. if (d_{1}, d_{2}, x, y) ∈ B, then for all x′, y′ ∈ ℕ, and d′_{i} ∈ D_{i}, if configurations (d_{i}, x, y), and (d′_{i}, x′, y′) of T_{i} are compatible, then there exists d′_{3−i} ∈ D_{3−i}, such that λ_{1}(d_{1}) = λ_{2}(d_{2}), and configurations (d_{3−i}, x, y), and (d′_{3−i}, x′, y′) of T_{3−i} are compatible, and (d′_{1}, d′_{2}, x′, y′) ∈ B.

[Definition 5] □

We say that two tiling systems are domino bisimilar if and only if there is a domino bisimulation relating them.

Theorem 6 (Undecidability of domino bisimilarity) Domino bisimilarity is undecidable for origin constrained tiling systems.

The proof is a reduction from the halting problem for deterministic 2-counter machines. For a deterministic 2-counter machine M we define in section 2.3 two origin constrained tiling systems T_{1}, and T_{2}, enjoying the following property.

Proposition 7 Machine M does not halt, if and only if there is a domino bisimulation relating T_{1} and T_{2}.

2.2 Counter machines

A 2-counter machine M consists of a finite program with the set L of instruction labels, and instructions of the form:

   • start:  goto ℓ
   •  ℓ:  c_{i} := c_{i} + 1; goto m
   •  ℓ:  if c_{i} = 0 then c_{i} := c_{i} + 1; goto m
                        else c_{i} := c_{i} - 1; goto n
   • halt:

where i = 1, 2; ℓ, m, n ∈ L, and {start, halt} ⊂ L. A configuration of M is a triple (ℓ, x, y) ∈ L×ℕ×ℕ, where ℓ is the label of the current instruction, and x, and y are the values stored in counters c_{1}, and c_{2}, respectively; we denote the set of configurations of M by Conf(M). The semantics of 2-counter machines is standard: let ⊢_{M} ⊆ Conf(M) × Conf(M) be the usual one-step derivation relation on configurations of M; by ⊢_{M}^{+} we denote the reachability (in at least one step) relation for configurations, i.e., the transitive closure of ⊢_{M}.

Before we give a reduction from the halting problem of 2-counter machines to origin constrained domino bisimilarity let us take a look at the directed graph (Conf(M), ⊢_{M}), with configurations of M as vertices, and edges denoting derivation in one step. Since machine M is deterministic, for each configuration there is at most one outgoing edge; moreover only halting configurations have no outgoing edges. It follows that connected components of the graph (Conf(M), ⊢_{M}) are either trees with edges going to the root which is the unique halting configuration in the component, or have no halting configuration at all. This observation implies the following proposition.

Proposition 8 Let M be a 2-counter machine. The following conditions are equivalent:

1. machine M halts on input (0, 0), i.e., (start, 0, 0) ⊢_{M}^{+} (halt, x, y) for some x, y ∈ ℕ,

2. (start, 0, 0) ∼_{M} (halt, x, y) for some x, y ∈ ℕ, where ∼_{M} ⊆ Conf(M) × Conf(M) is the symmetric, and transitive closure of ⊢_{M}.

2.3 The reduction

Now we go for a proof of Proposition 7. The idea is to design a tiling system which “simulates” behaviour of a 2-counter machine.

Let M be a 2-counter machine. We construct a tiling system T_{M} with the set L of instruction labels of M as the set of dominoes, and the identity function on L as the labelling function. Note that this implies that all tuples belonging to a domino bisimulation relating copies of T_{M} are of the form (ℓ, ℓ, x, y), so we can identify them with configurations of M, i.e., sometimes we will make no distinction between (ℓ, ℓ, x, y) and (ℓ, x, y) ∈ Conf(M) for ℓ ∈ L.

We define the horizontal compatibility relations H_{M}, H_{M}^{0} ⊆ L × L of the tiling system T_{M} as follows:

• (ℓ, m) ∈ H_{M} if and only if either of the instructions below is an instruction of machine M:

       – ℓ:  c_{1} := c_{1} + 1; goto m

–

         m:  if c_{1} = 0 then c_{1} := c_{1} + 1; goto n

                       else c_{1} := c_{1} - 1; goto ℓ

• (ℓ, m) ∈ H_{M}^{0} if and only if (ℓ, m) ∈ H_{M}, or the instruction below is an instruction of machine M:

–

         ℓ:  if c_{1} = 0 then c_{1} := c_{1} + 1; goto m

                      else c_{1} := c_{1} - 1; goto n

The vertical compatibility relations V_{M}, and V_{M}^{0} are defined in the same way, with c_{1} instructions replaced with c_{2} instructions. We also take D_{M}^{ori} = L, i.e., all dominoes are allowed in position (0, 0). Note that the identity function is a 1-1 correspondence between configurations of M, and configurations of the tiling system T_{M}; from now on we will hence identify configurations of M and T_{M}. It follows immediately from the construction of T_{M}, that two configurations c, c′ ∈ Conf(M) are compatible as configurations of T_{M}, if and only if c ⊢_{M} c′, or c′ ⊢_{M} c, i.e., compatibility relation of T_{M} coincides with the symmetric closure of ⊢_{M}. By ≈_{M} we denote the symmetric and transitive closure of the compatibility relation of T_{M}. The following proposition is then straightforward.

Proposition 9 The two relations ∼_{M}, and ≈_{M} coincide.

Now we are ready to define the two origin constrained tiling systems T_{1}, and T_{2}, postulated in Proposition 7. The idea is to have two independent and slightly pruned copies of T_{M} in T_{2}: one without the initial configuration (start, 0, 0), and the other without any halting configurations (halt, x, y). The other tiling system T_{1} is going to have three independent copies of T_{M}: the two of T_{2}, and moreover, another full copy of T_{M}.

More formally we define D_{2} = (L × {1, 2}) \ {(halt, 2)}, and D_{2}^{ori} = D_{2} \ {(start, 1)}, and V_{2} = ((V_{M} ⊗ 1) ∪ (V_{M} ⊗ 2)) ∩ (D_{2} × D_{2}), where for a binary relation R we define R⊗i to be the relation {((a, i), (b, i)) : (a, b) ∈ R}. The other compatibility relations V_{2}^{0}, H_{2}, and H_{2}^{0} are defined analogously from the respective compatibility relations of T_{M}.

The tiling system T_{1} is obtained from T_{2} by adding yet another independent copy of T_{M}, this time a complete one: D_{1} = D_{2} ∪ (L × {3}), and D_{1}^{ori} = D_{2}^{ori} ∪ (V_{M} ⊗ 3), and V_{1} = V_{2} ∪ (V_{M} ⊗ 3), etc. The labelling functions of T_{1}, and T_{2} are defined as λ_{i}((ℓ, i)) = ℓ.

In order to show Proposition 7 we establish the following two claims.

Claim 10 If machine M halts on input (0, 0), then there is no domino bisimulation relating T_{1} and T_{2}.

Proof: If B is a domino bisimulation relating T_{1} and T_{2}, then it must be the case that ((start, 3), (start, 2), 0, 0) ∈ B, since (start, 1) ∉ D_{2}^{ori}. But then using condition 3 of the definition of a domino bisimulation while “simulating” the halting computation of M in copy 3 of T_{1}, we conclude that we must have ((halt, 3), (halt, 2), x, y) ∈ B for some x, y ∈ ℕ, but this is impossible, since (halt, 2) ∉ D_{2}. [Claim 10] ■

Claim 11 If machine M does not halt on input (0, 0), then there is a domino bisimulation relating T_{1} and T_{2}.

Proof: Suppose that M does not halt on input (0, 0). We claim that the following relation B is a domino bisimulation for T_{1} and T_{2}:

{ ((ℓ, i), (ℓ, i), x, y) : i ∈ {1, 2} and ((ℓ, i), x, y) ∈ Conf(T_{1}) } ∪

{ ((ℓ, 1), (ℓ, 3), x, y) : (ℓ, x, y) ∼_{M} (halt, x′, y′) for some x′, y′ ∈ ℕ } ∪

{ ((ℓ, 2), (ℓ, 3), x, y) : (ℓ, x, y) ≁_{M} (halt, x′, y′) for all x′, y′ ∈ ℕ }.

Conditions 1. and 2. of the definition of a domino bisimulation, and condition 3. for the first component of the above union follow immediately. We check condition 3. for elements of the second and third components of the above union.

Suppose that ((ℓ, 1), (ℓ, 3), x, y) ∈ B; note that it suffices to check that (ℓ, x, y) is not compatible with (start, 0, 0), since copy 1 of T_{1} differs from copy 3 of T_{2} only in that it does not have (start, 0, 0) as a configuration. By definition of B we have that (ℓ, x, y) ∼_{M} (halt, x′, y′) for some x′, y′ ∈ ℕ, so the assumption that M does not halt on input (0, 0), and Proposition 8 imply that (start, 0, 0) ≁_{M} (ℓ, x, y). Then it follows by Proposition 9 that (start, 0, 0) ≉_{M} (ℓ, x, y), so in particular (ℓ, x, y) is not compatible with (start, 0, 0) and hence we are done.

The case for ((ℓ, 2), (ℓ, 3), x, y) ∈ B is similar. It suffices then to check that (ℓ, x, y) is not compatible with (halt, x′, y′) for any x′, y′ ∈ ℕ. This follows from Proposition 9 applied to the assumption that (ℓ, x, y) ≁_{M} (halt, x′, y′) for all x′, y′ ∈ ℕ. [Claim 11] ■

This concludes the proof of Theorem 6.

3 Hhp-bisimilarity is undecidable

The proof of Theorem 3 is a reduction from the problem of deciding bisimilarity for origin constrained tiling systems. A method of encoding a tiling system on an infinite grid in the graph of behaviours of a finite asynchronous transition system is due to Madhusudan and Thiagarajan [MT98]; we use a modified version of a gadget invented by them. For each origin constrained tiling system T we define an asynchronous transition system A(T), such that the following proposition holds.

Proposition 12 There is a domino bisimulation relating origin constrained tiling systems T_{1} and T_{2}, if and only if there is a hhp-bisimulation relating the asynchronous transition systems A(T_{1}) and A(T_{2}).

Let T = (D, D^{ori}, (H, H^{0}), (V, V^{0}), L, λ) be an origin constrained tiling system. We define the asynchronous transitions system A(T). The schematic structure of A(T) can be seen in Figure 1. The set of events is defined as:

E_{A(T)} = { x_{i}, y_{i} : i ∈ {0, 1, 2, 3} }
∪ \{ d_{ij}, \overline{d}_{ij} : i, j ∈ \{0, 1, 2\}, d ∈ D, and d ∈ D^{ori} if (i, j) = (0, 0) \}.

By abuse of notation we sometimes write d_{xy} or \overline{d}_{xy} for x, y ∈ ℕ; we always mean by that the events d_{x̂ŷ} or \overline{d}_{x̂ŷ}, respectively, where for z ∈ ℕ we define

ẑ = \begin{cases}z & if z ≤ 2, \\ 2 − (z mod 2) & if z > 2. \end{cases}

The labelling function replaces dominoes in “d”-, and “\overline{d}”-events, with their labels in the tiling system:

λ_{A(T)}(e) = \begin{cases}e & if e ∈ \{ x_{i}, y_{i} : i ∈ \{0, …, 3\} \}, \\ λ(d)_{ij} & if e = d_{ij}, for some d ∈ D, \\ \overline{λ(d)}_{ij} & if e = \overline{d}_{ij}, for some d ∈ D. \end{cases}

The states, events, and transitions of A(T) can be read from Figure 1; we briefly explain below how to do it.

There are sixteen states in the bottom layer of the structure in Figure 1(a). Let us identify these sixteen states with pairs of numbers shown on the vertical [figure: ◯; y_{3}; ◯; ◯; ◯; ◯; 0,3; ◯; 1,3; ◯; 2,3; ◯; 3,3; ◯; y_{2}; ◯; ◯; ◯; ◯; 0,2; ◯; 1,2; ◯; 2,2; ◯; 3,2; ◯; ◯; ◯; ◯; ◯; y_{1}; 0,1; ◯; 1,1; ◯; 2,1; ◯; 3,1; ◯; ◯; ◯; ◯; •; x_{0}; y_{0}; 0,0; ◯; x_{1}; 1,0; ◯; x_{2}; 2,0; ◯; x_{3}; 3,0]

(a) The structure of A(T) in the large.

[figure: ∘; ∘; ∘; ∘; ∘; ∘; ∘; ∘; y_{3}; x_{2}; ∘; ∘; ∘; x_{3}; y_{3}; ∘; ∘; g_{11}; f_{21}; d_{22}; ∘; e_{12}; g_{11}; f_{21}; ∘; y_{3}; x_{2}; g_{11}; f_{21}; d_{22}; _{\overline{f}_{21}}; ∘; x_{3}; y_{3}; _{\overline{g}_{11}}; e_{12}; g_{11}; f_{21}; ∘; ∘; x_{2}; y_{2}; ∘; ∘; ∘; x_{3}; y_{2}; ∘; ∘; ∘; ∘; ∘; ∘; ∘; ∘; _{d_{22}}; x_{2}; y_{2}; e_{12}; d_{22}; f_{21}; ∘; _{e_{12}}; x_{3}; y_{2}; g_{11}; e_{12}; d_{22}; ∘; f_{21}; d_{22}; e_{12}; ∘; g_{11}; e_{12}; d_{22}]

(b) The fine structure of the upper-right cube of A(T). Figure 1: The structure of the asynchronous transition system A(T). macro-arrows originating in these states shown in Figure 1(a). Each of these macro-arrows denotes a bundle of d_{ij}-, and \overline{d}_{ij}-event transitions sticking out of the state below, arranged in the fashion shown in Figure 1(b). For each state (i, j), and domino d ∈ D, there are d_{ij}-, and \overline{d}_{ij}-event transitions sticking out, and moreover for each state (i′, j′) from which there is an arrow in Figure 1(a) to state (i, j), there is a d_{i′j′}-event transition sticking out of (i, j). The state (0, 0) is exceptional: only dominoes from the origin constraint D^{ori} are allowed as events of transitions sticking out of it. It is also the initial state of A(T).

As can be seen in Figure 1(b), from both ends of the d_{ij}-event transition rooted in state (i, j), there is an x_{i}-event transition to the corresponding (bottom, or top) (i ⊕ 1, j) state, and an y_{i}-event transition to the corresponding (i, j ⊕ 1) state, where

i ⊕ 1 = \begin{cases}i + 1 & for i < 3, \\ 2 & for i = 3. \end{cases}

For each d_{i′j′}-event transition t sticking out of state (i, j), and each e ∈ D, there can be a pair of transitions which together with t and the \overline{e}_{ij}-event transition form a “diamond” of transitions; the events of the transitions lying on the opposite sides of the diamond coincide then. This type of transitions is shown in Figure 1(b) as dotted arrows. The condition for the two transitions closing the diamond to exist is that configurations (d, i′, j′) and (e, i′ + |i′ − i|, j′ + |j′ − j|) of T are compatible, or (i′, j′) = (i, j) and e = d. We define the independence relation I_{A(T)} ⊆ E_{A(T)} × E_{A(T)}, to be the symmetric closure of the set:

{ (x_{i}, y_{j}), (x_{i}, d_{ij}), (y_{j}, d_{ij}) : i, j ∈ {0, …, 3}, and d ∈ D } ∪
\{ (d_{ij}, \overline{d}_{ij}) : i, j ∈ \{0, …, 3\}, and d ∈ D \} ∪
\{ (d_{0j}, \overline{e}_{1j}) : j ∈ \{0, …, 3\}, and (d, e) ∈ H^{0} \} ∪
\{ (d_{ij}, \overline{e}_{(i+1)j}) : i ∈ \{1, 2, 3\}, j ∈ \{0, …, 3\}, and (d, e) ∈ H \}
\{ (d_{i0}, \overline{e}_{i1}) : i ∈ \{0, …, 3\}, and (d, e) ∈ V^{0} \} ∪
\{ (d_{ij}, \overline{e}_{i(j+1)}) : i ∈ \{0, …, 3\}, j ∈ \{1, 2, 3\}, and (d, e) ∈ V \}.

Note that it follows from the above that all diamonds of transitions in A(T) are in fact independence diamonds.

Proof (of Proposition 12) The idea is to show that every domino bisimulation for T_{1} and T_{2} gives rise to a hhp-bisimulation for A(T_{1}) and A(T_{2}), and vice versa. First observe, that a run of A(T_{i}) for i ∈ {1, 2} is uniquely determined by the numbers x and y of the occurrences of the x_{j}-events, and the y_{k}-events, respectively, and the set of its “d”- and “\overline{d}”-events, which is of size at most two. In other words, we can identify runs of A(T_{i}) with triples (F_{i}, x, y), where F_{i} ⊆ E_{A(T_{i})} contains at most two “d”- and “\overline{d}”-events, and x, y ∈ ℕ, and elements of a hhp-bisimulation relating A(T_{1}) and A(T_{2}) with quadruples (F_{1}, F_{2}, x, y). The following claim immediately implies Proposition 12.

Claim 13

1. Let B ⊆ Conf(A(T_{1}), A(T_{2})) be an hhp-bisimulation relating A(T_{1}) and A(T_{2}). Then the set \{ (d, e, x, y) : (\{\overline{d}_{xy}\}, \{\overline{e}_{xy}\}, x, y) ∈ B \} is a domino bisimulation for T_{1} and T_{2}.

2. Let B ⊆ Conf(T_{1}, T_{2}) be a domino bisimulation relating T_{1} and T_{2}. Then the set \{ (\{\overline{d}_{xy}\}, \{\overline{e}_{xy}\}, x, y) : (d, e, x, y) ∈ B \} can be extended to an hhp-bisimulation for A(T_{1}) and A(T_{2}).

Proof: Let B ⊆ Conf(A(T_{1}), A(T_{2})) be an hhp-bisimulation. We need to check that the set \{(d, d′, x, y) : (\{\overline{d}_{xy}\}, \{\overline{d′}_{xy}\}, x, y) ∈ B \} satisfies conditions 1.–3. of Definition 5. Conditions 1. and 2. follow easily by first applying condition 1. and then repeatedly applying condition 2., or condition 3. of Definition 2.

We argue that condition 3. of Definition 5 is satisfied as well. Without loss of generality assume that i = 1; the other case is symmetric. Let (\{\overline{d}_{xy}\}, \{\overline{e}_{xy}\}, x, y) ∈ B, and configurations (d, x, y) and (d′, x′, y′) of T_{1} be compatible. Let x′ = x + 1, and y′ = y; the other three cases are analogous.

From the construction of A(T_{1}) and A(T_{2}), and by condition 2. of Definition 2 it follows that (\{\overline{d}_{xy}, d_{xy}\}, \{\overline{e}_{xy}, e_{xy}\}, x, y) ∈ B. Hence by condition 5. of Definition 2 we have that ({d_{xy}}, {e_{xy}}, x, y) ∈ B, and by condition 2., that ({d_{xy}}, {e_{xy}}, x + 1, y) = ({d_{xy}}, {e_{xy}}, x′, y′) ∈ B.

If x > 0 then (d_{xy}, d′_{x′y′}) ∈ H_{T_{1}}, and if x = 0 then (d_{xy}, d′_{x′y′}) ∈ H_{T_{1}}^{0}. Hence by the construction of A(T_{1}) it follows that (\{d_{xy}, \overline{d′}_{x′y′}\}, x′, y′) is a run of A(T_{1}). Then condition 2. of Definition 2 implies that there is an e′ ∈ D_{T_{2}}, such that (\{e_{xy}, \overline{e′}_{x′y′}\}, x′, y′) is a run of A(T_{2}), and λ_{1}(d′) = λ_{2}(e′), and (\{d_{xy}, \overline{d′}_{x′y′}\}, \{e_{xy}, \overline{e′}_{x′y′}\}, x′, y′) ∈ B. Therefore, by condition 5. of Definition 2 we have that (\{\overline{d′}_{x′y′}\}, \{\overline{e′}_{x′y′}\}, x′, y′) ∈ B, and by construction of A(T_{2}) it follows that (d′, e′) ∈ H_{T_{2}} if x > 0, and (d′, e′) ∈ H_{T_{2}}^{0} if x = 0, i.e., configurations (e, x, y) and (e′, x′, y′) of T_{2} are compatible. This concludes the proof of clause 1. of the claim.

Now we sketch a proof of clause 2. of the claim. Note that the maximal runs of A(T_{i}) for i ∈ {1, 2} are of one of the following forms:

1. (\{d_{xy}, \overline{d}_{xy}\}, x, y),

2. (\{d_{(x−1)y}, \overline{d′}_{xy}\}, x, y), such that (d, d′) ∈ H_{T_{i}}^{0} if x = 1, and (d, d′) ∈ H_{T_{i}} if x > 1.

3. (\{d_{x(y−1)}, \overline{d′}_{xy}\}, x, y), such that (d, d′) ∈ V_{T_{i}}^{0} if y = 1, and (d, d′) ∈ V_{T_{i}} if y > 1.

Suppose B ⊆ D_{1} ×D_{2} ×ℕ×ℕ is a domino bisimulation relating T_{1} and T_{2}. To get an hhp-bisimulation \overline{B} ⊆ Run (A(T_{1})) × Run (A(T_{2})) we do the following:

1. add to \overline{B} all the tuples (\{d_{xy}, \overline{d}_{xy}\}, \{e_{xy}, \overline{e}_{xy}\}, x, y), such that (d, e, x, y) ∈ B,

2. add to \overline{B} all the tuples (\{d_{(x−1)y}, \overline{d′}_{xy}\}, \{e_{(x−1)y}, \overline{e′}_{xy}\}, x, y), such that (d, e, x − 1, y) ∈ B and (d′, e′, x, y) ∈ B, and moreover, (d, x − 1, y) and (d′, x, y) are compatible as configurations of T_{1}, and (e, x − 1, y) and (e′, x, y) are compatible as configurations of T_{2},

3. add to \overline{B} all the tuples (\{d_{x(y−1)}, \overline{d′}_{xy}\}, \{e_{x(y−1)}, \overline{e′}_{xy}\}, x, y), such that (d, e, x, y − 1) ∈ B and (d′, e′, x, y) ∈ B, and moreover, (d, x, y − 1) and (d′, x, y) are compatible as configurations of T_{1}, and (e, x − 1, y) and (e′, x, y) are compatible as configurations of T_{2},

4. close \overline{B} “downwards”, i.e., complete it so that condition 5. of the Definition 2 is satisfied.

We leave it as an exercise to the Reader to check that \overline{B} is indeed an hhpbisimulation. [Claim 13] ■ [Proposition 12] ■

This concludes the proof of Theorem 3.

4 A 1-safe Petri net

An attentive Reader might have noticed, that the asynchronous transitions system A(T) as described in the previous section, and sketched in Figure 1, is not coherent, while all asynchronous transition systems derived from (1-safe) Petri nets are [WN95, NW96]. It turns out, however, that A(T) is not far from being coherent: it suffices to close all the diamonds with events d_{ij}, and x_{i} in positions (i, j ⊕ 1), and with events d_{ij}, and y_{j} in positions (i ⊕ 1, j), for i, j ∈ {0, …, 3}; note that runs ending at the top of these diamonds are maximal runs. This completion of the transition structure of A(T) does not affect the arguments used to establish Claim 13, and hence Theorem 3, but since it would obscure the picture in Figure 1(b), we have decided not to draw it there.

Our aim now is to present a finite 1-safe Petri net N(T) whose derived asynchronous transition system is isomorphic to the completion of A(T) mentioned above. The set of transitions of the net N(T) is just the set of events of the asynchronous transitions system A(T). The structure of the net N(T) is shown in Figure 2. The operation k ⊖ 1 for k ∈ {0, 1, 2} is defined as follows:

[figure: •; •; _{\overline{x}_{0}}; •; _{\overline{y}_{0}}; •; •; x_{0}; x_{0}; y_{0}; •; y_{0}; _{\overline{x}_{1}}; _{\overline{y}_{1}}; x_{1}; x_{1}; y_{1}; y_{1}; _{\overline{x}_{2}}; _{\overline{y}_{2}}; x_{2}; x_{2}; y_{2}; y_{2}; x_{3}; y_{3}]

[figure: •; #; x_{i}; d_{ij}; y_{j}; •; d_{ij}]

For all d ∈ D, and i, j ∈ {0, 1, 2}, such that (i, j) = (0, 0) implies d ∈ D^{ori}.

[figure: •; e_{(i⊖1)(j⊖1)}; •; f_{ij}; _{\overline{x}_{i}}; _{\overline{d}_{ij}}; _{\overline{y}_{j}}; •; g_{(i⊖1)j}; •; h_{i(j⊖1)}] For all d, …, h ∈ D, and i, j ∈ {0, 1, 2},

such that (i, j) = (0, 0) implies d ∈ D^{ori}, and:

• f ≠ d,

• (g, d) ∉ H^{0}, if i ⊖ 1 = 0, and (g, d) ∉ H, if i ⊖ 1 > 0,

• (h, d) ∉ V^{0}, if j ⊖ 1 = 0, and (h, d) ∉ V, if j ⊖ 1 > 0.

Figure 2: The structure of the 1-safe Petri net N(T).

k ⊖ 1 = \begin{cases}undefined & for k = 0, \\ 0 or 2 & for k = 1, \\ 1 & for k = 2. \end{cases}

For example a transition \overline{d}_{12} has arrows from places e_{01} and e_{21} for all e ∈ D, because possible values for (1 ⊖ 1, 2 ⊖ 1) are (0, 1) and (2, 1).

We leave it as an exercise for the Reader to check that there is indeed a 1-1 correspondence between firing sequences of the Petri net N(T), and runs of (a completion—mentioned above—of) the asynchronous transition system A(T), and this correspondence also respects the independence structure of the Petri net and the asynchronous transition system. Let us only give a few remarks on the design of N(T):

• The place # serves as a resource shared by all “d_{ij}”-events for all i, j ∈ {0, 1, 2}, and hence guarantees “mutual exclusion” of these events. Note that for example if the place # was not connected to events d_{11} and e_{21} for some d ≠ e, then they could both occur in a configuration of N(T).

• For every configuration C of N(T) we have that n ∈ ℕ is the number of occurrences of x_{i}-events, and m ∈ ℕ is the number of occurrences of y_{j}-events in C for i, j ∈ {0, 1, 2, 3}, if and only if there is a token in place \overline{x}n̂, and there is a token in place \overline{y}m̂ in the marking of N(T) corresponding to C, or an event \overline{d}_{nm} occurs in C.

• Arrows from places x_{i} for i ∈ {0, 1, 2} to events x_{i+1}, and arrows from places y_{j} for j ∈ {0, 1, 2} to events y_{i+1}, together with the arrows from places x_{i} and y_{j} to events d_{ij}, guarantee that the N(T) counterparts of configurations ({d_{xy}}, x + 1, y + 1) of A(T) are maximal.

References

[Bed88] Marek A. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, 1988.

[Bed91] Marek A. Bednarczyk. Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdańsk, April 1991. Avail-

        able electronically at http://www.ipipan.gda.pl/~marek.

[FH99] Sibylle Fröschle and Thomas Hildebrandt. On plain and hereditary history preserving bisimulation. To apper in Proceedings of Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS’99, Szklarska Por_{}eba, Poland, September 1999.

[Frö99] Sibylle Fröschle. Decidability of plain and hereditary historypreserving bisimilarity for BPP. To be presented at 6th International Workshop on Expressiveness in Concurrency, EXPRESS’99, Eindhoven, The Netherlands, August 1999.

[JM96] Lalita Jategaonkar and Albert R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154:107–143, 1996.

[JNW96] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996. A preliminary version appeared in Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science, pages 418– 427, Montreal, Canada, June 1993. IEEE Computer Society Press.

[MT98] P. Madhusudan and P. S. Thiagarajan. Controllers for discrete event systems via morphisms. In Davide Sangiorgi and Robert de Simone, editors, CONCUR’98, Concurrency Theory, 9th International Conference, Proceedings, volume 1466 of LNCS, pages 18–33, Nice, France, September 1998. Springer.

[NC95] M. Nielsen and C. Clausen. Games and logics for a noninterleaving bisimulation. Nordic Journal of Computing, 2(2):221–249, 1995.

[NW96] Mogens Nielsen and Glynn Winskel. Petri nets and bisimulation. Theoretical Computer Science, 153(1–2):211–244, 1996.

[RT88] A. Rabinovich and B. Trakhtenbrot. Behaviour structures and nets of processes. Fundamenta Informaticae, 11:357–404, 1988.

[Shi85] M. W. Shields. Concurrent machines. Computer Journal, 28:449– 465, 1985.

[vGG89] Rob van Glabbeek and Ursula Goltz. Equivalence notions for concurrent systems and refinement of actions (Extended abstract). In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, volume 379 of LNCS, pages 237–248, Por _{}abka-Kozubnik, Poland, August/September 1989. Springer-Verlag.

[Vog91] Walter Vogler. Deciding history preserving bisimilarity. In Javier Leach Albert, Burkhard Monien, and Mario Rodríguez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, ICALP’91, volume 510 of LNCS, pages 493– 505, Madrid, Spain, 8–12 July 1991. Springer-Verlag.

[WN95] Glynn Winskel and Mogens Nielsen. Models for concurrency. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, Semantic Modelling, pages 1–148. Oxford University Press, 1995.

Recent BRICS Report Series Publications

RS-99-19 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Bisimilarity is Undecidable. June 1999. 18 pp.

RS-99-18 M. Oliver Möller and Harald Rueß. Solving Bit-Vector Equations of Fixed and Non-Fixed Size. June 1999. 18 pp. Revised version of an article appearing under the title Solving Bit-Vector Equations in Gopalakrishnan and Windley, editors, Formal Methods in Computer-Aided Design: Second International Conference, FMCAD ’98 Proceedings, LNCS 1522, 1998, pages 36–48.

RS-99-17 Andrzej Filinski. A Semantic Account of Type-Directed Partial Evaluation. June 1999. To appear in Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, PPDP99 ’99 Proceedings, LNCS, 1999.

RS-99-16 Rune B. Lyngsø and Christian N. S. Pedersen. Protein Folding in the 2D HP Model. June 1999. 15 pp.

RS-99-15 Rune B. Lyngsø, Michael Zuker, and Christian N. S. Pedersen. An Improved Algorithm for RNA Secondary Structure Prediction. May 1999. 24 pp. An alloy of two articles appearing in Istrail, Pevzner and Waterman, editors, Third Annual International Conference on Computational Molecular Biology, RE-COMB 99 Proceedings, 1999, pages 260–267, and Bioinformatics, 15, 1999.

RS-99-14 Marcelo P. Fiore, Gian Luca Cattani, and Glynn Winskel. Weak Bisimulation and Open Maps. May 1999. To appear in Longo, editor, Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS ’99 Proceedings, 1999.

RS-99-13 Rasmus Pagh. Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions. May 1999. 11 pp. A short version to appear in Algorithms and Data Structures: 6th International Workshop, WADS ’99 Proceedings, LNCS, 1999.

RS-99-12 Gerth Stølting Brodal, Rune B. Lyngsø, Christian N. S. Pedersen, and Jens Stoye. Finding Maximal Pairs with Bounded Gap. April 1999. 31 pp. To appear in Combinatorial Pattern Matching: 10th Annual Symposium, CPM ’99 Proceedings, LNCS,