Date: Fri, 7 Jun 91 02:36:18 -0700
From: Rob van Glabbeek <rvg@Sunburn.Stanford.EDU>
To: pratt@cs.stanford.edu
Subject: bisimulations for higher dimensional automata

Below I define the notion of bisimulation equivalence (and some
related notions) for cubical sets (with initial state, final state,
and labeling). I found it convenient to use a concrete representation
rather then any of the two abstract ones (note that all the morphism
information in the category of cubical sets is encoded in the 4
commutativities between s and t; a morphism that in one of your
earlier mails was encoded as 001TT1T0 corresponds to
s(0,s(1,t(2,t(5,(s(7))))))). I'm curious if more abstract and elegant
definitions of bisimulation will turn out to be possible when working
in a more abstract and elegant notion of cubical set.
-r

A higher dimensional automata, labeled over an alphabet A, is a
7-tuple (Q, d, s, t, I, F l) where
- Q is a set (of states),
- d: Q -> Nat (associating to each state q a dimension d(q); states of
  dimension 0 may be called nodes, states of dimension 1 are edges, states
  of dimension n represent lists of n transitions firing concurrently),
- s,t: Nat*Q -> Q are partial functions (s(k,q) indicates the start and
  t(q,k) the termination of the k-th transition in the list of
  transitions q) satisfying:
	     s(k,q) defined <=> t(k,q) defined <=> k < d(q)
	     k < d(q) => d(s(k,q)) = d(t(k,q)) = d(q)-1
	     i =< j => s(j,(s(i,q)) = s(i,s(j+1,q))
	     i =< j => s(j,(t(i,q)) = t(i,s(j+1,q))
	     i =< j => t(j,(s(i,q)) = s(i,t(j+1,q))
	     i =< j => t(j,(t(i,q)) = t(i,t(j+1,q))
  (These requirements say that s(k, ) and t(k, ) applied to a state q
  representing a list of d(q) > k transitions yield states
  representing lists of d(q)-1 transitions obtained by leaving out
  transition number k and renumbering the transitions with number > k.
  s(0, ) and t(0, ) applied on edges just yield the begin and endnodes
  of those edges),
- I is an element of Q with d(I)=0 (the initial state),
- F is a subset of Q whose members q satisfy d(q)=0 (the set of final states),
- l: Q -> A is a partial function (the labeling function) defined on
  states of dimension 1, satisfying:
	     d(q)=2 and (k=0 or k=1) => l(s(k,q))=l(t(k,q))
  (this requirement says that opposite edges in a square have the same
  label. This because they represent the same transition, scheduled
  either before or after the firing of another transition. Transitions
  or events can be defined as equivalence classes of edges (with
  respect to the finest equivalence identifying s(k,q) and t(k,q) for
  any q with d(q)=2 and (k=0 or k=1)), and represent occurrences of
  actions (elements of A) indicated by their label).

Let (Q,d,s,t,I,F,l) be a higher dimensional automaton. The projection
function p: Nat*Q -> Q is a partial function defined by
- p(k,q) = s(0,s(1,...s(k-1,s(k+1,...s(d(q)-1,q)...))...)) if k < d(q)
- p(k,q) undefined if k >= d(q).
Of course d(p(k,q))=1 and s(0,d(p(i,q)))=s(0,d(p(j,q))) for i,j,k < d(q).
Now the labeling function can be extended to a total function l: Q -> A*
by defining:  l(q) = l(p(0,q)) l(s(0,q))  if  d(q) > 1, and
	      l(q) = the empty string	  if  d(q) = 0.

A path in a higher dimensional automaton (Q,d,s,t,I,F,l) is a sequence
p(0) p(1)  ... p(n) in Q* (n >= 0) such that for any 0<i<n+1 there is
a k in Nat such that p(i-1)=s(k,p(i)) or p(i)=t(k,p(i-1)).
Two paths P and P' are adjacent - notation P <-> P' - if there are
paths Q,R and states p,p' such that d(p) differs from d(p') and P=QpR
while P'=Qp'R.
A path P' is an extension of a path P - notation P < P' - if there is
a path Q with P'=PQ.

A bisimulation between two higher dimensional automata (Q,d,s,t,I,F,l)
and (Q',d',s',t',I',F',l') labeled over A is a binary relation R
between their paths, such that: 
- their initial states (viewed as paths) are related,
- if (p(0) p(1)  ... p(n)) R (q(0) q(1)  ... q(m)) then n=m, p(n) in F
  <=> q(n) in F', and for 0 =< k =< n: l(p(k)) = l'(q(k))  (and thus
  d(p(k)) = d'(p(k))), 
- if P R Q and P <-> P' then there is a Q' with Q <-> Q' and P' R Q',
- if P R Q and Q <-> Q' then there is a P' with P <-> P' and P' R Q',
- if P R Q and P < P' then there is a Q' with Q < Q' and P' R Q',
- if P R Q and Q < Q' then there is a P' with P < P' and P' R Q'.

Two higher dimensional automata are bisimulation equivalent if there
exists a bisimulation between them. Note that bisimulation equivalence
is an equivalence indeed. For 1-dimensional automata (with d(q)<2
for all q in Q) a path is just an alternating sequence of nodes and
edges - each edge going from the node before it to the node after it,
no two paths are adjacent and the notion of bisimulation equivalence
defined above coincides with the classical one.

Let A = (Q,d,s,t,I,F,l) be a higher dimensional automaton. Homotopy is
the smallest equivalence realtion on the paths of A containing
adjacency. The unfolding U(A) of A is defined as the automaton
(Q',d',s',t',I',F',l'), where:
- Q' is the set of all paths in A starting at I, modulo homotopy,
- d'[p(1)...p(n)] = d(p(n)),
- s'([p(1)...p(n)],k) = {q(1)...q(n-1) | q(1)...q(n-1)p(n) is homotopic
  with p(1)...p(n) and s(p(n),k)=q(n-1)},
- t'([p(1)...p(n)],k) = [p(1)...p(n) t(p(n),k)],
- I' = [I],
- F' = {[p(1)...p(n)] | p(n) in F},
- l'[p(1)...p(n)] = l(p(n)).
It is straightforward to check that U(A) is well-defined and is an
automata indeed. 

Two higher dimensional automata (Q,d,s,t,I,F,l) and
(Q',d',s',t',I',F',l') labeled over A are isomorph if there exists a
bijection f: Q -> Q' (an isomorphism) satisfying:
- d'(f(q)) = d(q), f(I)=I', f(q) in F' <=> q in F, l'(f(q))=l(q),
- {s'(k,f(q)) | k < d(q)} = {f(s(k,q)) | k < d(q)} and
- {t'(k,f(q)) | k < d(q)} = {f(t(k,q)) | k < d(q)}.
The weak requirements for s and t allow to change the order in the
list of transitions represented by a state.

Proposition: U(U(A)) and U(A) are isomorph, and two higher
dimensional automata have isomorph unfoldings iff there is a
bijective bisimulation between them. 
Proof: Straightforward.