Bisimilarity of Open Terms


Rensink, Arend (2000) Bisimilarity of Open Terms. Information and Computation, 156 (1-2). pp. 345-385. ISSN 0890-5401

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:Traditionally, in process calculi, relations over open terms, i.e., terms with free process variables, are defined as extensions of closed-term relations: two open terms are related if and only if all their closed instantiations are related. Working in the context of bisimulation, in this paper we study a different approach; 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, one giving rise to De Simone's formal hypothesis bisimilarity and the other to a variation which we call hypothesis-preserving bisimilarity (denoted ~fh and ~hp, respectively). For open terms, we have (strict) inclusions ~fh c ~hp c ~ci (the latter denoting the standard “closed instance” extension); for closed terms, the three coincide. Each of these relations is a congruence in the usual sense. We also give an alternative characterisation of ~hp in terms of nonconditional transitions, as substitution-closed bisimilarity (denoted ~sb). Finally, we study the issue of recursion congruence: we prove that each of the above relations is a congruence with respect to the recursion operator; however, for ~ci this result holds under more restrictive conditions than for ~fh and ~hp.
Item Type:Article
Copyright:© 2000 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