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.