Bisimilarity of open terms

Traditionally, in process calculi, relations over open terms, i.e., terms w ith free process variables, are defined as extensions of closed-term relati ons: two open terms are related if and only if all their closed instantiati ons are related. Working in the context of bisimulation, in this paper we s tudy a different approach; we define semantic models for open terms, so-cal led conditional transition systems, and define bisimulation directly on tho se models. It turns out that this can be done in at least two different way s, one giving rise to De Simone's formal hypothesis bisimilarity and the ot her to a variation which we call hypothesis-preserving bisimilarity (denote d similar to(fh) and similar to(hp), respectively). For open terms, we have (strict) inclusions similar to(fh)subset of(hP)subset of(ci) (the latter d enoting the standard "closed instance" extension); for closed terms, the th ree coincide. Each of these relations is a congruence in the usual sense. W e also give an alternative characterisation of similar to(hp) in terms of n onconditional transitions, as substitution-closed bisimilarity (denoted sim ilar to(sb)). Finally, we study the issue of recursion congruence: we prove that each of the above relations is a congruence with respect to the recur sion operator; however, for similar to(ci) this result holds under more res trictive conditions than for similar to(fh) and similar to(hp) (C) 2000 Aca demic Press.