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 names and 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 named sets, the basic building blocks of HD-automata, a notion of 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.
Available as PDF (198 kB, no cover)
Download BibTeX entry.