Bisimilarity of Open Terms


Rensink, Arend (1997) Bisimilarity of Open Terms. In: Expressiveness in Concurrency, EXPRESS '97, 8-12 September 1997, Ligure, Italy (pp. pp. 262-285).

open access
Abstract:The standard way of lifting a binary relation, R, from closed terms of an algebra to open terms is to define its closed-instance extension, R_{ci}, which holds for a given pair of open terms if and only if R holds for all their closed instantiations. In this paper, we study alternatives for the case of (strong) bisimulation: we define semantic models for open terms, so-called conditional transition systems, and define bisimulation directly on those models. It turns out that this can be done in at least two different ways, giving rise to formal hypothesis bisimulation \sim_{fh} (due to De Simone) and hypothesis-preserving bisimilarity \sim_{hp}. For open terms, we have (strict) inclusions \sim_{fh} \subset \sim_{hp} \subset \sim_{ci}; for closed terms, the three relations coincide. We show that each of these relations is a congruence in the usual sense, and we give an alternative characterisation of \sim_{hp} in terms of non-conditional transitions. Finally, we study the issue of recursive congruence: we give general theorems for the congruence of each of the above variants with respect to the recursion combinator, where, however, the results we achieve for \sim_{fh} and \sim_{hp} hold in a more general setting than the one for \sim_{ci}.
Item Type:Conference or Workshop Item
Copyright:© 1997 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page