@TechReport{	  it:2005-037,
  author	= {Marino Miculan and Emilio Tuosto and Kidane Yemane},
  title		= {{HD}-Automata for Open Bisimulation},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2005},
  number	= {2005-037},
  month		= nov,
  abstract	= {HD-automata are a syntax-independent operational model
		  introduced for dealing with history-dependent formalisms.
		  This kind of enriched automata, where states, transitions,
		  and labels are equipped with \emph{names} and
		  \emph{symmetries}, have been successfully applied for
		  modelling early and late bisimulation in $\pi$-calculus and
		  hyperbisimulation in Fusion calculus. However, current
		  HD-automata are not adequate for modelling open
		  bisimulation, because in HD-automata two names cannot be
		  unified, while open bisimulation is closed under all
		  possible name substitution respecting name distinctions. In
		  this paper we tackle the problem by integrating in the
		  definition of \emph{named sets}, the basic building blocks
		  of HD-automata, a notion of \emph{distinction:} names can
		  coalesce if the distinction allows to. Then, we use
		  HD-automata over named sets with distinctions for modelling
		  the open bisimulation of $\pi$-calculus. Finally, we
		  discuss the relationship between named sets with
		  distinctions and their HD-automata, with the categorical
		  counterparts based on presheaf categories.}
}