Date: Fri, 7 Jun 91 02:36:18 -0700
From: Rob van Glabbeek
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* 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.
*