Bisimilarity of Open Terms
Rensink, Arend (1997) Bisimilarity of Open Terms. In: Expressiveness in Concurrency, EXPRESS '97, 8-12 September 1997, Ligure, Italy.
|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_, 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 _ (due to De Simone) and hypothesis-preserving bisimilarity _. For open terms, we have (strict) inclusions _ _ _; 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 _ 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 _ and _ hold in a more general setting than the one for _.
|Item Type:||Conference or Workshop Item|
|Copyright:||© 1997 Elsevier|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/66671|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page