×

Bisimilarity of open terms. (English) Zbl 0911.68066

Palamidessi, C. (ed.) et al., EXPRESS ’97. Papers from the conference, Santa Margherita Ligure, Italy, September 8–12, 1997. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 7, 25 p. (1997).
Summary: 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 \({\overset {fh}\sim}\) (due to De Simone) and hypothesis-preserving bisimilarity \({\overset {hp}\sim}\). For open terms, we have (strict) inclusions \({\overset {fh}\sim}\in {\overset {hp}\sim}\in {\overset {ci}\sim}\); for closed terms, the three relations coincide. We how that each of these relations is a congruence in the usual sense, and we give an alternative characterisation of \({\overset {hp}\sim}\) 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 \({\overset {fh}\sim}\) and \({\overset {hp}\sim}\) hold in a more general setting than the one for \({\overset {ci}\sim}\).
For the entire collection see [Zbl 0903.00061].

MSC:

68W10 Parallel algorithms in computer science
68U20 Simulation (MSC2010)
PDFBibTeX XMLCite
Full Text: Link