BRICS RS-99-1 Jurdziński & Nielsen: Hereditary History Preserving Simulation is Undecidable BRICS

Basic Research in Computer Science

Hereditary History Preserving Simulation is Undecidable

Marcin Jurdziński Mogens Nielsen BRICS Report Series RS-99-1 ISSN 0909-0878 January 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/1/

Hereditary History Preserving Simulation Is Undecidable

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

January 1999

Abstract

We show undecidability of hereditary history preserving simulation for finite asynchronous transition systems by a reduction from the halting problem of deterministic Turing machines. To make the proof more transparent we introduce an intermediate problem of deciding the winner in domino snake games. First we reduce the halting problem of deterministic Turing machines to domino snake games. Then we show how to model a domino snake game by a hereditary history simulation game on a pair of finite asynchronous transition systems.

1 Domino snake games

A tiling system D = (D, V, H) consists of a set D of dominoes, and two relations: V ⊆ D^{2}, called vertical compatibility, and H ⊆ D^{2}, called horizontal compatibility. Intuitively, one can think of dominoes as unit squares with coloured sides (and with an orientation, i.e., the dominoes cannot be rotated.) In this metaphor the meaning of the vertical and horizontal compatibility relations can be described as follows: for a pair of dominoes d, d′ ∈ D, we have

• (d, d′) ∈ V, if the top side of d has the same color as the bottom side of d′,

• (d, d′) ∈ H, if the right-hand side of d has the same color as the left-hand side of d′.

∗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.

Definition 1 (Domino snake game) Let D = (D, V, H) be a tiling system, and let ℕ_{+}^{2}, the positive quadrant of the integer grid, be the set of locations. Pairs (l, d) ∈ ℕ_{+}^{2} × D are called configurations. Locations l = (i, j) and l′ = (i′, j′) are neighbouring, if |i−i′|+ |j − j′| = 1. Configurations (l, d) and (l′, d′) are consistent, if their locations l and l′ are neighbouring, and the adjecent sides have the same color, e.g.: if i′ = i + 1 and j′ = j, then (d, d′) ∈ H; if i′ = i and j′ = j − 1, then (d′, d) ∈ V; etc. The domino snake game Γ_{ds}(D) is played by two players Tiler and Challenger.

1. First the players fix an initial configuration: Challenger chooses a location l ∈ ℕ_{+}^{2}, and then Tiler responds by picking a domino d ∈ D; the pair (l, d) becomes the current configuration.

2. In each move of the game the players change the current configuration (l, d): first Challenger chooses a location l′ ∈ L neighbouring with l, and then Tiler responds by picking a domino d′, so that configurations (l, d) and (l′, d′) are consistent.

A play is a maximal sequence of configurations formed by players making moves in the fashion described above. Challenger wins a play if after a finite number of moves Tiler gets stuck, i.e., he cannot complete a move. Otherwise the play is infinite and Tiler is the winner.

Let d^{init} ∈ D be a domino. In the origin constrained domino snake game Γ_{ds}(D, d^{init}) Tiler’s responses in the “origin” location (1, 1) are restricted only to domino d^{init}; we refer to d^{init} ∈ D as the origin constraint of the game Γ_{ds}(D, d^{init}). [Definition 1] □

A strategy for Tiler in Γ_{ds}(D, d^{init}) is a partial function Θ : ℕ_{+}^{2} ∪ (ℕ_{+}^{2} × D × ℕ_{+}^{2}) ⇀ D, such that:

1. if Θ((1, 1)), or Θ(l, d, (1, 1)) are defined, then they are equal to d^{init},

2. if Θ(l, d, l′) = d′, and locations l and l′ are neighbouring, then configurations (l, d) and (l′, d′) are consistent.

A play ⟨(l_{0}, d_{0}), (l_{1}, d_{1}), (l_{2}, d_{2}), … ⟩ is consistent with a strategy Θ, if d_{0} = Θ(l_{0}), and d_{i+1} = Θ(l_{i}, d_{i}, l_{i+1}) for all i ≥ 0. A strategy Θ is winning for Tiler if all plays consistent with Θ are infinite, i.e., winning for Tiler. The notion of a (winning) strategy for Challenger can be defined appropriately. We say that a map Θ : ℕ_{+}^{2} → ℘(D) is closed for Γ_{ds}(D, d^{init}) if:

1. Θ(l) ≠ ∅ for all l ∈ ℕ_{+}^{2}, and Θ((1, 1)) = {d^{init}},

2. if d ∈ Θ(l), then for all locations l′ neighbouring with l, there is d′ ∈ Θ(l′), so that configurations (l, d) and (l′, d′) are consistent.

Proposition 2 Tiler has a winning strategy in Γ_{ds}(D, d^{init}) if and only if there is a closed map for Γ_{ds}(D, d^{init}).

Domino snake games are easily seen to be determined, i.e., either of the two players has a winning strategy. The problem of deciding the winner in an origin constrained domino snake game is the following: given a tiling system D = (D, V, H), and an origin constraint d^{init} ∈ D, decide which of the players has a winning strategy in the game Γ_{ds}(D, d^{init}).

Theorem 3 (Undecidability of domino snake games) The problem of deciding the winner in origin constrained domino snake games is undecidable.

The proof is a reduction from the halting problem for deterministic inputless Turing machines. For a deterministic inputless Turing machine M we define a tiling system D_{M} = (D_{M}, V_{M}, H_{M}), and an origin constraint d_{M} ∈ D_{M}, enjoing the following property.

Proposition 4 Machine M halts if and only if Challenger has a winning strategy in the origin constrained domino snake game Γ_{ds}(D_{M}, d_{M}).

Let M = (Q, q^{init}, q^{halt}, Σ, δ) be a 1-tape, deterministic Turing machine, where Q is the finite set of states, q^{init} ∈ Q is the initial state, q^{halt} ∈ Q is the halting state, Σ is the tape alphabet, and δ : Q × Σ → Q × Σ × {−1, 1} is the transition function. The semantics is standard:

• the machine starts working at time t = 1 and in state q^{init} scanning cell c = 1 of an empty tape (containing the special blank symbol ⊔ ∈ Σ in all cells),

• if the machine at time t is in state q and scans cell c containing symbol σ, then it writes symbol σ′ into cell c, and at time t + 1 it is in state q′ and scans cell c + d, where δ(q, σ) = (q′, σ′, d).

Without loss of generality we may assume that the machine never moves its head to the left of the first cell of the tape.

For technical convenience we assume that the transition function δ of machine M is total; this makes machine M loop forever in fact. We say that machine M halts if its computation reaches the halting state in a finite number of steps; otherwise we say that it loops. Clearly, the question if a deterministic inputless Turing machine halts in this sense is undecidable.

By Γ = (Q×Σ)∪Σ∪{⊥} we denote the set of cell contents of machine M, extended with a special symbol ⊥ ∉ Σ. Let C_{M} : ℕ^{2} → Γ be the unbounded

⊥
⊥ (q^{init}, ⊔) ⊔ ⊔
⊥  q^{init}  ⊥ ⊥ ⊥

Figure 1: The initial fragment of the computation table of an inputless Turing machine.

computation table of M (see Figure 1):

C_{M}(c, t) = \begin{cases}q^{init} & if c = 1 and t = 0, \\ ⊥ & if c = 0, or t = 0 and c ≥ 2, \\ the contents of cell c at time t & otherwise. \end{cases}

It is an easy and standard observation (see [Pap94], page 168) that if M is deterministic, then for c, t ≥ 1 it holds that

C_{M}(c, t) is uniquely determined by

– C_{M}(c − 1, t − 1), C_{M}(c, t − 1), and C_{M}(c + 1, t − 1), if c ≥ 2, and

– C_{M}(c, t − 1), and C_{M}(c + 1, t − 1), if c = 1.

(1)

Let Δ : Γ^{3} ⇀ Γ be a (partial) function yielding this unique value. For technical reasons (see the proof of Claim 7) we require that

if β = ⊥ and Δ(α, β, γ) is defined, then γ = ⊥.  (2)

The function Δ can be easily computed from the transition function δ of machine M.

We adopt the following notational convention: a lower case Greek letter with a bar denotes a pair of triples of cell contents

γ̄ = (γ_{−1}, γ_{0}) ∈ (Γ^{3})^{2}, where γ_{t} = (γ_{i,−1}, γ_{i,0}, γ_{i,1}) ∈ Γ^{3}, for i ∈ {−1, 0}.

We say that γ̄ ∈ (Γ^{3})^{2} is a peephole, if

γ_{0,0} = Δ(γ_{−1});

we denote the set of peepholes by Π. A peephole γ is halting if γ_{i,d} = (q^{halt}, σ) for some i ∈ {−1, 0}, d ∈ {−1, 0, 1}, and σ ∈ Σ, otherwise it is live; we denote the set of live peepholes by Λ. The peephole table P_{M} : ℕ_{+}^{2} → Π of machine M is defined for all (c, t) ∈ ℕ_{+}^{2} by

P_{M}(c, t) = γ̄, where γ_{i,d} = C_{M}(c + d, t + i),

for i ∈ {−1, 0}, and d ∈ {−1, 0, 1}, i.e., its value in location (c, t) is a 3 × 2 fragment of the computation table to the left, to the right, and below (c, t).

Definition 5 (Peephole snake game Γ_{ds}(D_{M}, d_{M})) The peephole tiling system D_{M} is defined to be the triple (Λ, V_{M}, H_{M}), where

• (τ̄, γ̄) ∈ V_{M} if τ_{0} = γ_{−1}, and

• (τ̄, γ̄) ∈ H_{M} if τ_{i,d+1} = γ_{i,d} for all i, d ∈ {−1, 0}.

In other words, the dominoes of the peephole tiling system are the live peepholes, and the vertical and horizontal compatibility relations ensure, that two peepholes are compatible if their “overlapping” parts coincide. The origin constraint d_{M} ∈ D is the value of the peephole table for the “origin” location (1, 1), i.e., d_{M} = ((⊥, q^{init}, ⊥), (⊥, (q^{init}, ⊔), ⊔)); see Figure 1. [Definition 5] □

Proof (of Proposition 4)

Tiler wins if M loops: If machine M does not halt then its computation table C_{M} does not contain the halting state, hence its peephole table P_{M} contains only live peepholes. Tiler has then a winning strategy consisting in choosing always the value of the peephole table P_{M}(c, t) for the current location (c, t).

Challenger wins if M halts: We say that a configuration ((c, t), γ̄) is incorrect, if for some d ∈ {−1, 0, 1} we have γ_{−1,d} ≠ C_{M}(c + d, t − 1) and c + d ≥ 1.

If machine M halts then there is a location (c, t) with c ≥ 1, so that C_{M}(c, t) = (q^{halt}, σ) for some σ ∈ Σ. Challenger picks (c, t + 1) as the initial location, and so the initial configuration must be incorrect since Tiler can only respond with live peepholes. The following two claims give Challenger a strategy to maintain an incorrect configuration as an invariant, while progressing towards the “origin” location (1, 1). This clearly gives a winning strategy for Challenger, because the origin constraint allows only the value of the peephole table P_{M}(1, 1) in location (1, 1), which clearly is not incorrect.

Claim 6 If the current configuration ((c, t), γ̄) with t ≥ 2 is incorrect, then Challenger can in no more than two moves either make Tiler stuck, or force the play to an incorrect configuration ((c′, t − 1), γ̄′).

Proof: By the definition of an incorrect configuration we have that γ_{−1,d} ≠ C_{M}(c + d, t − 1) for some d ∈ {−1, 0, 1}, so that c + d ≥ 1. Challenger in no more than two moves makes Tiler stuck or forces ((c + d, t − 1), γ̄′) to be a new configuration. By the definition of V_{M} and H_{M} we have γ′_{0,0} = γ_{−1,d} ≠ C_{M}(c+d, t−1), hence from (1) and the definition of a peephole it follows that the new configuration must be incorrect. [Claim 6] ■

Claim 7 If the current configuration ((c, 1), γ̄) with c ≥ 2 is incorrect, then Challenger by moving to location (c − 1, 1) either makes Tiler stuck, or forces the new configuration ((c − 1, 1), γ̄′) to be incorrect.

Proof: If γ_{−1,−1} ≠ C_{M}(c − 1, 0), or γ_{−1,0} ≠ C_{M}(c, 0), then by the definition of H_{M} the next configuration ((c − 1, 1), γ̄′) must be incorrect. Otherwise γ_{−1,0} = ⊥, hence (2) implies that γ_{−1,1} = ⊥, but this is impossible because ((c, 1), γ̄) is incorrect. [Claim 7] ■ [Proposition 4] ■

2 Hereditary history preserving simulation

Definition 8 (Labelled asynchronous transition system) A labelled asynchronous transition system is a tuple A = (S, s^{init}, E, →, L, λ, I), where S is its set of states, s^{init} ∈ 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′′,

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

s′′ ∈ S. [Definition 8] □

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

Let A = (S, s^{init}, E, →, L, λ, I) be a labelled asynchronous transition system. A sequence of events ē = ⟨e_{1}, e_{2}, …, e_{k}⟩ ∈ E^{k} is a path in A if there are states s_{1}, s_{2}, …, s_{k+1} ∈ S, such that s_{1} = s^{init}, and for all i ∈ [k] we have t_{i} = (s_{i}, e_{i}, s_{i+1}) for some t_{i} ∈ T. We denote the set of paths in A by Path(A). For every sequence of events ē ∈ E^{k} the independence relation induces an E-labelled partial order π(ē) = ([k], ⊴, ε), where ε : [k] → E is the labelling function. For all i ∈ [k] we set ε(i) = e_{i}. For i, j ∈ [k] we define i ⋖ j to hold, if i ≤ j, and (e_{i}, e_{j}) ∉ I. We get ⊴ as the transitive closure of ⋖.

For ē, ē′ ∈ Path(A) we define ē ≅ ē′ to hold, if the corresponding labelled partial orders π(ē) and π(ē′) are isomorphic. This is clearly an equivalence relation.

Definition 9 (Unfolding) Let A = (S, s^{init}, E, →, L, λ, I) be a labelled asynchronous transition system. The unfolding of A is the labelled asynchronous transition system U(A) = (S_{U(A)}, s_{U(A)}^{init}, E, →_{U(A)}, L, λ, I), defined as follows:

• the set of states S_{U(A)} is defined to be Path(A)/≅, i.e., the set of (Elabelled) partial order behaviours of A,

• the initial state s_{U(A)}^{init} is [ϵ]≅, i.e., the empty (E-labelled) partial order,

• we define τ →^{e}_{U(A)} τ′ to hold, if ē ∈ τ, and ē · e ∈ τ′, for some path ē ∈ Path(A).

Definition 10 (Hereditary history preserving simulation game) Let A_{i} = (S_{i}, s_{i}, E_{i}, →_{i}, L, λ_{i}, I_{i}) for i = 1, 2 be labelled asynchronous transition systems. The hereditary history preserving simulation game Γ_{hhps}(A_{1}, A_{2}) is played by two players Spoiler and Simulator on the arena based on the unfoldings U(A_{1}), and U(A_{2}).

A τ_{i} ∈ S_{U(A_{i})} can be seen an E_{i}-labelled partial order (|τ_{i}|, ⊴_{i}, ε_{i}), where |τ_{i}| is the underlying set of τ_{i}, and ε_{i} : |τ_{i}| → E_{i} is the labelling function. By λ_{i}(τ_{i}) we denote the L-labelled partial order (|τ_{i}|, ⊴_{i}, λ_{i} ∘ ε_{i}). The arena of Γ_{hhps}(A_{1}, A_{2}) is the labelled transition system

(S_{(A_{1},A_{2})}, (∅, ∅, ∅), E_{1} × E_{2}, →_{(A_{1},A_{2})} ),

defined as follows:

• the set of states S_{(A_{1},A_{2})} is the set of triples (τ_{1}, Ξ, τ_{2}), where τ_{1} ∈ S_{U(A_{1})}, τ_{2} ∈ S_{U(A_{2})}, and Ξ : |τ_{1}| → |τ_{2}| is an isomorphism of L-labelled partial orders λ_{1}(τ_{1}) and λ_{2}(τ_{2}),

• we define (τ_{1}, Ξ, τ_{2}) ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} (τ′_{1}, Ξ′, τ′_{2}) to hold, if τ_{1} →^{e_{1}}_{U(A_{1})} τ′_{1}, and

τ_{2} →^{e_{2}}_{U(A_{2})} τ′_{2}, and Ξ ⊆ Ξ′, i.e., Ξ′ is the unique extension of Ξ obtained by mapping the latest occurrence of the e_{1} event in τ′_{1} to the latest occurrence of the e_{2} event in τ′_{2}.

We call the elements of S_{(A_{1},A_{2})} configurations of the game. The initial state (∅, ∅, ∅) is the initial configuration. In every move the players change the current configuration (τ_{1}, Ξ, τ_{2}) into the next configuration (τ′_{1}, Ξ′, τ′_{2}) in one of the following ways.

1. First Spoiler picks an e_{1} ∈ E_{1} so that τ′_{1} →^{e_{1}}_{U(A_{1})} τ_{1}. Then Simulator has to respond with the e_{2} ∈ E_{2}, such that τ′_{2} →^{e_{2}}_{U(A_{2})} τ_{2}, and

(τ′_{1}, Ξ′, τ′_{2}) ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} (τ_{1}, Ξ, τ_{2}).

Note that Simulator has no choice here: his response is uniquely determined as the label of Ξ(p) in τ_{2}, where p ∈ |τ_{1}| is the latest occurrence of an e_{1} event in τ_{1}.

2. First Spoiler picks an e_{1} ∈ E_{1} so that τ_{1} →^{e_{1}}_{U(A_{1})} τ′_{1}. Then Simulator has to respond with an e_{2} ∈ E_{2}, such that τ_{2} →^{e_{2}}_{U(A_{2})} τ′_{2}, and

(τ_{1}, Ξ, τ_{2}) ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} (τ′_{1}, Ξ′, τ′_{2}).

A play is a maximal sequence of configurations formed by players making moves in the fashion described above. Spoiler wins a play if after a finite number of moves Simulator gets stuck, i.e., he cannot complete a move. Otherwise the play is infinite and Simulator is the winner. [Definition 10] □

Note that if C ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} C′, then configuration C′ is uniquely determined by C, e_{1}, and e_{2}; and vice versa, configuration C is uniquely determined from C′, e_{1}, and e_{2}. Based on this we define partial operations ⊕ : S_{(A_{1},A_{2})}×(E_{1}×E_{2}) ⇀ S_{(A_{1},A_{2})}, and ⊖ : S_{(A_{1},A_{2})} × (E_{1} × E_{2}) ⇀ S_{(A_{1},A_{2})},

• C ⊕ (e_{1}, e_{2}) = C′, if C ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} C′,

• C ⊖ (e_{1}, e_{2}) = C′, if C′ ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} C.

A strategy for Simulator in Γ_{hhps}(A_{1}, A_{2}) is a function Σ : S_{(A_{1},A_{2})} × E_{1} → ℘(E_{2}), such that if e_{2} ∈ Σ(C, e_{1}), then C ⊕ (e_{1}, e_{2}) is defined. Let C_{i} = (τ_{1}^{i}, Ξ^{i}, τ_{2}^{i}) for i ≥ 0 be configurations of Γ_{hhps}(A_{1}, A_{2}). A play ⟨C_{0}, C_{1}, C_{2}, …⟩ is consistent with a strategy Σ, if for all i ≥ 0 such that C_{i+1} = C_{i} ⊕ (e_{1}, e_{2}) (i.e., the i-th move is of type 2.), we have e_{2} ∈ Σ(C_{i}, e_{1}). A strategy Σ is winning for Simulator if all plays consistent with Σ are infinite, i.e., winning for Simulator.

We say that a strategy Σ : S_{(A_{1},A_{2})} ×E_{1} → ℘(E_{2}) is defined in a configura-

tion (τ_{1}, Ξ, τ_{2}), if Σ((τ_{1}, Ξ, τ_{2}), e_{1}) ≠ ∅ for all e_{1} ∈ E_{1}, such that τ_{1} →^{e_{1}}_{U(A_{1})} τ′_{1}.

We say that a strategy Σ is closed if it satisfies the following conditions:

1. Σ is defined in the initial configuration (∅, ∅, ∅),

2. if Σ is defined in C, and C ⊕ (e_{1}, e_{2}) is defined, then Σ is defined in C ⊕ (e_{1}, e_{2}),

3. if Σ is defined in C, and C ⊖ (e_{1}, e_{2}) is defined, then Σ is defined in C ⊖ (e_{1}, e_{2}).

The following follows easily from the definitions.

Proposition 11 Every closed strategy is winning for Simulator. Moreover, if Simulator has a winning strategy then he also has a closed one.

Theorem 12 (Undecidability of hhp-simulation) Hereditary history preserving simulation for finite labelled asynchronous transition systems is undecidable.

The proof is a reduction from the problem of deciding the winner in origin constrained domino snake games. The method is essentially due to Madhusudan and Thiagarajan [MT98]; we use a slightly modified version of a gadget invented by them.

Let Γ_{ds}(D, d^{init}) be an origin constrained domino snake game, where D = (D, V, H) is a tiling system, and d^{init} ∈ D is an origin constraint. We define a pair of finite labelled asynchronous transition systems: A_{C} “modelling” Challenger, and A_{T} “modelling” Tiler, so that the following property holds.

Proposition 13 Simulator has a winning strategy in Γ_{hhps}(A_{C}, A_{T}) if and only if Tiler has a winning strategy in the origin constrained domino snake game Γ_{ds}(D, d^{init}). □

Labelled asynchronous transition system

A_{C} = (S_{C}, s_{C}^{init}, E_{C}, →_{C}, L_{C}, λ_{C}, I_{C}) The states, events, and transitions of A_{C} can be read from Figure 2; we briefly explain below how to do it. The initial state is denoted by a solid circle (see Figure 2(a)). The set of events of A_{C} is defined as:

E_{C} = { x_{i}, y_{i} : i ∈ {0, 1, 2} } ∪ {?_{ij}, ¿_{ij} : i, j ∈ {0, 1, 2} }.

In Figure 2(b) we provide the detailed view of the upper-right cube of the schematic picture of A_{C} from Figure 2(a). The Reader can reconstruct the details of the remaining three cubes in Figure 2(a) by taking appropriately prunned and relabelled copies of the graph in Figure 2(b). For example, there are only two “question” events (instead of four as typical in Figure 2(b)), sticking out from the initial state, namely ¿_{00}, and ?_{00}. From a state which is at the bottom of a “double” vertical arrow labelled with “i, 0” for i ∈ {1, 2}, there are three events sticking out, namely: ¿_{i0}, ?_{i0}, and ?_{(i⊖1)0}, where

(i ⊖ 1) =^{df} 2 − (i mod 2). Similarly, from a state which is at the bottom of a “double” vertical arrow labelled with “0, j” for j ∈ {1, 2}, there are three events sticking out, namely: ¿_{0j}, ?_{0j}, and ?_{0(j⊖1)}. Finally, we obtain the whole transition graph of A_{C} by gluing together the appropriate faces of the four cubes. We have decided not to draw the whole picture in detail as it would be hard to digest. For example, as the result of the merge, there are six “question” events sticking out of the state at the bottom of the “triple” arrow labelled with “1, 1”, namely: ¿_{11}, ?_{11}, ?_{01}, ?_{10}, ?_{21}, and ?_{12}.

As the set of labels L_{C} we take the set of events E_{C}; we set the identity function on E_{C} as the labelling λ_{C}. As the independence relation I_{C} we take the symmetric closure of the set:

\begin{matrix}\{ (x_{i}, y_{j}), (x_{i},?_{ij}), (y_{j},?_{ij}) : i, j ∈ \{0, 1, 2\} \} ∪ \\ \{ (?_{ij}, ¿_{ij}), (?_{ij}, ¿_{(i⊕1)j}), (?_{ij}, ¿_{i(j⊕1)}) : i, j ∈ \{0, 1, 2\} \}, \end{matrix}  (3)

[figure: ◯; ◯; ◯; ◯; y_{2}; 0,2; ◯; 1,2; ◯; 2,2; ◯; ◯; ◯; ◯; y_{1}; 0,1; ◯; 1,1; ◯; 2,1; ◯; ◯; ◯; •; x_{0}; y_{0}; 0,0; ◯; x_{1}; 1,0; ◯; x_{2}; 2,0]

(a) The structure of A_{C} and A_{T} in the large.

[figure: ∘; ∘; ∘; ∘; ∘; ∘; ∘; ∘; y_{2}; x_{1}; ∘; _{¿_{12}}; ∘; _{¿_{22}}; ∘; x_{2}; y_{2}; ∘; ∘; ?_{22}; ?_{12}; ?_{11}; ∘; ?_{21}; ?_{22}; ?_{12}; ∘; y_{2}; x_{1}; ?_{22}; ?_{12}; ?_{11}; _{¿_{12}}; ∘; x_{2}; y_{2}; _{¿_{22}}; ?_{21}; ?_{22}; ?_{12}; ∘; _{¿_{11}}; ∘; x_{1}; y_{1}; ∘; ∘; ∘; x_{2}; y_{1}; ∘; _{¿_{21}}; ∘; ∘; ∘; ∘; ∘; ∘; ∘; _{¿_{11}}; x_{1}; y_{1}; ?_{21}; ?_{11}; ?_{12}; ∘; _{¿_{21}}; x_{2}; y_{1}; ?_{22}; ?_{21}; ?_{11}; ∘; ?_{12}; ?_{11}; ?_{21}; ∘; ?_{22}; ?_{21}; ?_{11}]

(b) The structure of the upper-right cube of A_{C} in detail. Figure 2: The structure of asynchronous transition systems A_{C} and A_{T}. where (i ⊕ 1) =^{df} 2 − ((i + 1) mod 2). Note, that this implies that all the “diamonds” in the transition graph of A_{C} are in fact independence squares.

Labelled asynchronous transition system

A_{T} = (S_{T}, s_{T}^{init}, E_{T}, →_{T}, L_{T}, λ_{T}, I_{T}) The overall structure of the transition graph of A_{T} is very similar to A_{C}. Indeed, Figure 2(a) serves as its schematic picture for both A_{C} and A_{T}. The set of events of A_{T} is defined as:

E_{T} = { x_{i}, y_{i} : i = 0, 1, 2 }
∪ {!_{ij}^{d}, ¡_{ij}^{d} : i, j ∈ {0, 1, 2}, d ∈ D, such that (i, j) ≠ (0, 0), or d = d^{init} }.

The notable difference with A_{C} is that every “question” event is replaced by |D| copies of a corresponding “answer” events, one for each element d of the set of dominoes D. As for the transition graph of A_{T}, it very closely mimicks the transition graph of A_{C}; every “question” event transition in A_{C} has its |D| “answer” counterparts in A_{T}. The only exception is the initial state of A_{T}, from which only two events stick out, namely: ¡_{00}^{d^{init}}, and !_{00}^{d^{init}}. This is how the origin constraint of the domino snake game (D, d^{init}) is encoded in A_{T}.

As the set of labels L_{T} we take again the set E_{C} of events of A_{C}. The labelling function maps the “answer” events to their “question” counterparts:

λ_{T}(e) = \begin{cases}e & if e ∈ \{ x_{i}, y_{i} : i ∈ \{0, 1, 2\} \}, \\ ?_{ij} & if e = !_{ij}^{d}, for some d ∈ D, \\ ¿_{ij} & if e = ¡_{ij}^{d}, for some d ∈ D. \end{cases}

The independence relation I_{T} is defined as the symmetric closure of the set:

{ (x_{i}, y_{j}), (x_{i},!_{ij}^{d}), (y_{j},!_{ij}^{d}) : i, j ∈ {0, 1, 2}, and d ∈ D } ∪
{ (!_{ij}^{d}, ¡_{ij}^{d}) : i, j ∈ {0, 1, 2}, and d ∈ D } ∪
{ (!_{ij}^{b}, ¡_{i(j⊕1)}^{d}) : i, j ∈ {0, 1, 2}, b, d ∈ D, and (b, d) ∈ V } ∪
{ (!_{ij}^{c}, ¡_{(i⊕1)j}^{d}) : i, j ∈ {0, 1, 2}, c, d ∈ D, and (c, d) ∈ H }.

(4)

Note how the vertical, and horizontal compatibility relations V, and H of the tiling system D are encoded in the independence relation I_{T} of the asynchronous transition system A_{T}. Figures 3(a–c) contain some close-ups of the fine structure of the transition graph of A_{T}. We adopt the convention that the dotted arrows in Figures 3(b–c) exist if and only if the corresponding events are independent according to I_{T}.

Proof (of Proposition 13) The idea of the proof is to show that winning strategies for Simulator in

[figure: ∘; ◯; ∘; _{¡{d^{init} \atop 00}}; ≡; ∘; _{!{d^{init} \atop 00}}; •; 0,0; •; _{!{d^{init} \atop 00}}; _{¡{d^{init} \atop 00}}]

(a) The single arrow “0, 0”.

[figure: ∘; ∘; ◯; ∘; ∘; _{¡{d \atop 0j}}; ≡; ∘; ◯; 0,j; ∘; _{!{d \atop 0j}}; _{!{b \atop 0(j⊖1)}}; _{¡{d \atop 0j}}]

(b) A double arrow “0, j”, for j ∈ {1, 2}.

[figure: ∘; ∘; ∘; ◯; ∘; ∘; ∘; _{¡{d \atop ij}}; ≡; ∘; ◯; i,j; ∘; _{!{c \atop (i⊖1)j}}; _{!{d \atop ij}}; _{!{b \atop i(j⊖1)}}; _{¡{d \atop ij}}] Variables b, c, and d range the set of

dominoes D.

(!_{ij}^{d}, ¡_{ij}^{d}) ∈ I_{T} for all d ∈ D
(!_{i(j⊖1)}^{b}, ¡_{ij}^{d}) ∈ I_{T} iff (b, d) ∈ V
(!_{(i⊖1)j}^{c}, ¡_{ij}^{d}) ∈ I_{T} iff (c, d) ∈ H

where (i ⊖ 1) =^{df} (i mod 2) + 1.

(c) A triple arrow “i, j”, seen as a part of the upper-right cube in Figure 2(a).

Figure 3: Details of the asynchronous transitions system A_{T}.

Γ_{hhps}(A_{C}, A_{T}), and winning strategies for Tiler in Γ_{ds}(D, d^{init}) can be mutually simulated. This idea is captured in the two translations below, one yielding a closed map for Γ_{ds}(D, d^{init}), given a closed strategy for Simulator in Γ_{hhps}(A_{C}, A_{T}), and the other yielding a closed strategy for Simulator in Γ_{hhps}(A_{C}, A_{T}), given a closed map for Γ_{ds}(D, d^{init}). By Propositions 11 and 2, and by determinacy of both domino snake, and hereditary history preserving simulation games, these translations suffice to establish Proposition 13.

By E_{?} we denote the set { ?_{ij}, ¿_{ij} : i, j ∈ {0, 1, 2} }, and by E_{!} the set {!_{ij}^{d}, ¡_{ij}^{d} : i, j ∈ {0, 1, 2}, and d ∈ D }. Let π_{T} = (|π_{T} |, ⊴_{T} , ε_{T}) be a state of U(A_{T}); we write

• #_{x}(π_{T}) for |ε_{T}^{−1}({x_{0}, x_{1}, x_{2}})|,

• #_{y}(π_{T}) for |ε_{T}^{−1}({y_{0}, y_{1}, y_{2}})|.

It is not hard to see that if (π_{C}, Ξ, π_{T}) is a configuration of Γ_{hhps}(A_{C}, A_{T}), then

1. π_{C} is uniquely determined by π_{T}, (in fact, π_{C} is isomorphic to λ_{T}(π_{T})),

2. π_{T} is uniquely determined by #_{x}(π), #_{y}(π), and by ε_{T} ∘ ε_{T}^{−1}(E_{!}) ⊆ E_{!},

3. |ε_{T}^{−1}(E_{!})| = |ε ∘ ε_{T}^{−1}(E_{!})| ≤ 2.

Properties 1. and 2. amount to saying that the number of occurrences of “x” events, the number of occurrences of “y” events, and the set of occurrences of “!” events in the E_{T}-labelled partial order π_{T} ∈ S_{U(A_{T})}, uniquely determine the configuration (π_{C}, Ξ, π_{T}) ∈ S_{(A_{C},A_{T})}. Property 3. implies that if |ε_{T}^{−1}(E_{!})| = 2, then (π_{C}, Ξ, π_{T}) is a maximal configuration. It follows that a strategy for Simulator in Γ_{hhps}(A_{C}, A_{T}) can be represented as a function:

Ω : ℕ_{+}^{2} × ({∅} ∪ E_{!}) × E_{?} → ℘(E_{!}).

For notational convenience, if l = (m, n) ∈ ℕ_{+}^{2}, then we write ?_{l} to denote ?_{ij}, and ¿_{l} to denote ¿_{ij}, where i = (m mod 2), and j = (n mod 2). Similarly, we write !_{l}^{d} for !_{ij}^{d}, and ¡_{l}^{d} for ¡_{ij}^{d}, where i = 2 − (m mod 2), and j = 2 − (n mod 2).

Tiler wins Γ_{ds}(D, d^{init}) if Simulator wins Γ_{hhps}(A_{C}, A_{T}): Suppose that Simulator has a closed strategy Ω : ℕ_{+}^{2}×({∅}∪E_{!})×E_{?} → ℘(E_{!}) in Γ_{hhps}(A_{C}, A_{T}). We define a map Θ : ℕ_{+}^{2} → ℘(D) in the following way:

Θ(l) = { d ∈ D : !_{l}^{d} ∈ Ω(l, ∅,?_{l}) }

for all l ∈ ℕ_{+}^{2}. It can be verified that Θ is a closed map for Γ_{ds}(D, d^{init}).

Simulator wins Γ_{hhps}(A_{C}, A_{T}) if Tiler wins Γ_{ds}(D, d^{init}): Suppose that there is a closed map Θ : ℕ_{+}^{2} → ℘(D) for Γ_{ds}(D, d^{init}). We define a strategy Ω : ℕ_{+}^{2} × ({∅} ∪ E_{!}) × E_{?} → ℘(E_{!}) for Simulator in the following way:

• Ω(l, ∅,?_{l}) = {!_{l}^{d} : d ∈ Θ(l) }, and Ω(l, ∅, ¿_{l}) = { ¡_{l}^{d} : d ∈ Θ(l) },

• Ω(l, ∅,?_{(l−δ)}) = {!_{(l−δ)}^{d} : d ∈ Θ(l − δ) },

• Ω(l, ¡_{l}^{d},?_{(l−δ)}) = {!_{(l−δ)}^{d} : d ∈ Θ(l − δ) }, and Ω(l,!_{l−δ}^{d}, ¿_{l}) = { ¡_{l}^{d} : d ∈ Θ(l) }.

for l ∈ ℕ_{+}^{2}, and δ ∈ {(0, 1), (1, 0)}. We skip the verification that Ω indeed gives rise to a closed strategy for Simulator in Γ_{hhps}(A_{C}, A_{T}). [Proposition 13] ■

The definition and some results on the hereditary history preserving bisimulation can be found in [Bed91, NC94, JNW96].

Definition 14 (Hereditary history preserving bisimulation game) The hereditary history preserving bisimulation game Γ_{hhpb}(A_{1}, A_{2}) is played by two players: Spoiler and Bisimulator. The only differences with respect to the hereditary history preserving simulation game Γ_{hhps}(A_{1}, A_{2}) are that Simulator is replaced by Bisimulator, and an extra kind of move is allowed.

3. First Spoiler picks an e_{2} ∈ E_{2} so that τ_{2} →^{e_{2}}_{U(A_{2})} τ′_{2}. Then Simulator has to respond with an e_{1} ∈ E_{1}, such that τ_{1} →^{e_{1}}_{U(A_{1})} τ′_{1}, and

(τ_{1}, Ξ, τ_{2}) ⟶^{(e_{1},e_{2})}_{(A_{1},A_{2})} (τ′_{1}, Ξ′, τ′_{2}).

We get the (plain) history preserving bisimulation game [RT88, vGG89] by allowing only the use of moves of type 2. and 3. [Definition 14] □

Plain history preserving bisimulation is known to be decidable [Vog91, JM96].

Problem 1 Is the problem of deciding the winner in hereditary history preserving bisimulation games decidable?

References

[Bed91] Marek A. Bednarczyk. Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Instytut Podstaw Informatyki PAN, filia w Gdańsku, April 1991. Available electronically at

        http://www.ipipan.gda.pl/~marek.

[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.

[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.

[NC94] Mogens Nielsen and Christian Clausen. Bisimulations, games and logic. Technical Report RS-94-6, Basic Research in Computer Science, Department of Computer Science, University of Aarhus, April 1994.

[Pap94] Christos H. Papadimitriou. Computational Complexity. Addison Wesley, 1994.

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

[vGG89] Rob van Glabbek and Ursula Goltz. Equivalence notions for concurrent sysmtes 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, Auotamata, Languages and Programming, 18th International Colloqium, ICALP’91, volume 510 of LNCS, pages 493–505, Madrid, Spain, 8–12 July 1991. Springer-Verlag.

Recent BRICS Report Series Publications

RS-99-1 Hereditary History Preserving Simulation is Undecidable. Nielsen, Mogens and Jurdziński, Marcin. January 1999. 15 pp.

RS-98-55 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects (Revised Report). December 1998. iv+75 pp. This is a revision of Technical Report 429, University of Cambridge Computer Laboratory, June 1997, and the earlier BRICS report RS-97-19, July 1997. Appears in Ramesh and Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FST&TCS ’97 Proceedings, LNCS 1346, 1997, pages 74–87.

RS-98-54 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. December 1998. 55 pp. To appear in Theoretical Computer Science.

RS-98-53 Julian C. Bradfield. Fixpoint Alternation: Arithmetic, Transition Systems, and the Binary Tree. December 1998. 20 pp.

RS-98-52 Josva Kleist and Davide Sangiorgi. Imperative Objects and Mobile Processes. December 1998. 22 pp. Appears in Gries and de Roever, editors, IFIP Working Conference on Programming Concepts and Methods, PROCOMET ’98 Proceedings, 1998, pages 285–303.

RS-98-51 Peter Krogsgaard Jensen. Automated Modeling of Real-Time Implementation. December 1998. 9 pp. Appears in The 13th IEEE Conference on Automated Software Engineering, ASE ’98 Doctoral Symposium Proceedings, 1998, pages 17–20.

RS-98-50 Luca Aceto and Anna Ingólfsdóttir. Testing Hennessy-Milner Logic with Recursion. December 1998. 15 pp. Appears in Thomas, editor, Foundations of Software Science and Computation Structures: Second International Conference, FoSSaCS ’99 Proceedings, LNCS 1578, 1999, pages 41–55.