Bisimilarity of open terms.

*(English)*Zbl 1046.68626Summary: 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 and the other to a variation which we call hypothesis-preserving bisimilarity. For open terms, we have (strict) inclusions between the relations; for closed terms, the three coincide. Each of these relations is a congruence in the usual sense. We also give an alternative characterisation of history-preserving bisimilarity in terms of non-conditional transitions, as substitution-closed bisimilarity. 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 closed-instance bisimilarity this result holds under more restrictive conditions than for the hypothesis-based variants.

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

68Q60 | Specification and verification (program logics, model checking, etc.) |

##### Software:

LOTOS
PDF
BibTeX
XML
Cite

\textit{A. Rensink}, Inf. Comput. 156, No. 1--2, 345--385 (2000; Zbl 1046.68626)

Full Text:
DOI

##### References:

[1] | Abramsky, S., A domain equation for bisimulation, Inform. and comput., 92, 161-218, (1991) · Zbl 0718.68057 |

[2] | Aceto, L, Bloom, B, and, Vaandrager, F. 1999, Checking open equations in GSOS systems, Draft. |

[3] | Aceto, L.; Hennessy, M.C.B., Termination, deadlock, and divergence, J. assoc. comput. Mach., 39, 147-187, (1992) · Zbl 0799.68131 |

[4] | Baeten, J.C.M.; Weijland, W.P., Process algebra, (1990), Cambridge Univ. Press Cambridge · Zbl 0716.68002 |

[5] | Baldamus, M.; Dingel, J., Modal characterization of weak bisimulation for higher-order processes, (), 285-296 |

[6] | Barendregt, H.P., The lambda calculus, Studies in logic and the foundations of mathematics, 103, (1984), North-Holland Amsterdam · Zbl 0551.03007 |

[7] | Bloom, B., Structural operational semantics for weak bisimulation, Theoret. comput. sci., 146, 25-685, (1995) |

[8] | Bloom, B.; Istrail, S.; Meyer, A.R., Bisimulation can’t be traced, J. assoc. comput. Mach., 42, 232-268, (1995) · Zbl 0886.68027 |

[9] | Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Comput. networks ISDN systems, 14, 25-59, (1987) |

[10] | Brinksma, E., On the uniqueness of fixpoints modulo observation congruence, () |

[11] | Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, J. assoc. comput. Mach., 31, 560-599, (1984) · Zbl 0628.68025 |

[12] | Cardelli, L., Type systems, () |

[13] | Cleaveland, W.R., Concur ’92, Lecture notes in computer science, 630, (1992), Springer-Verlag New York/Berlin |

[14] | De Simone, R., Higher-level synchronising devices in meije-SCCS, Theoret. comput. sci., 37, 245-267, (1985) · Zbl 0598.68027 |

[15] | Fokkink, W., On the completeness of the equations for the Kleene star in bisimulation, Algebraic methodology and software technology, Lecture notes in computer science, 1101, (1996), p. 180-194 · Zbl 0886.03032 |

[16] | Fokkink, W.; van Glabbeek, R., Ntyft/ntyxt rules reduce to ntree rules, Inform. and comput., 126, 1-10, (1996) · Zbl 0853.68124 |

[17] | Fokkink, W.; Verhoef, C., A conservative look at operational semantics with variable binding, Inform. and comput., 146, 24-54, (1998) · Zbl 0916.68098 |

[18] | Gadducci, F.; Montanari, U., Tiles, rewriting rules and CCS, (), 1-19 · Zbl 0917.68115 |

[19] | Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, Cambridge tracts in theoretical computer science, 7, (1989), Cambridge Univ. Press Cambridge |

[20] | van Glabbeek, R.J., The linear time-branching time spectrum, (), 278-297 |

[21] | van Glabbeek, R.J., A complete axiomatization for branching bisimulation congruence of finite-state behaviours, (), 473-484 |

[22] | van Glabbeek, R.J., The linear time-branching time spectrum II: the semantics of sequential systems with silent moves, (), 66-81 |

[23] | van Glabbeek, R.J.; Goltz, U., Equivalence notions for concurrent systems and refinement of actions, (), 237-248 · Zbl 0755.68095 |

[24] | Gordon, A.D., Bisimilarity as a theory of functional programming, Electron. notes in theoret. comput. sci., 1, (1995) · Zbl 0910.68118 |

[25] | Groote, J.F.; Vaandrager, F.W., Structured operational semantics and bisimulation as a congruence, Inform. and comput., 100, 202-260, (1992) · Zbl 0752.68053 |

[26] | Hennessy, M.C.B.; Lin, H., Symbolic bisimulations, Theoret. comput. sci., 138, 353-389, (1995) · Zbl 0874.68187 |

[27] | Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs · Zbl 0637.68007 |

[28] | Howe, D.J., Proving congruences of bisimulation in functional programming languages, Inform. and comput., 124, 103-112, (1996) · Zbl 0853.68073 |

[29] | Larsen, K.G., Compositional theories based on an operational semantics of contexts, (), 487-518 |

[30] | Larsen, K.G.; Xinxin, L., Compositionality through an operational semantics of contexts, J. logic comput., 1, 761-795, (1991) · Zbl 0738.68056 |

[31] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 73-155, (1992) · Zbl 0758.68043 |

[32] | Milner, R., A complete inference system for a class of regular behaviours, J. comput. syst. sci., 28, 439-466, (1984) · Zbl 0562.68065 |

[33] | Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs · Zbl 0683.68008 |

[34] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I and II, Inform. and comput., 100, 1-77, (1992) |

[35] | Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695 |

[36] | Milner, R.; Sangiorgi, D., The problem of “weak bisimulation up to”, () |

[37] | Mitchell, J.C., Type systems for programming languages, (), 365-458 · Zbl 0900.68122 |

[38] | Montanari, U.; Pistore, M.; Yankelevich, D., Efficient minimization up to location equivalence, (), 265-279 |

[39] | Mukund, M.; Nielsen, M., CCS, locations and asynchronous transition systems, (), 328-341 |

[40] | Parrow, J.; Victor, B., The fusion calculus: expressiveness and symmetry in mobile processes, Symposium on logic in computer science, (1998), Comput. Soc. Press New York |

[41] | Sands, D., From SOS rules to proof principles: an operational metatheory for functional languages, 24TH ACM SIGPLAN-SIGACT symposium on principles of programming languages, (1997), ACM New York |

[42] | Sangiorgi, D., Bisimulation for higher-order calculi, Inform. and comput., 131, 141-178, (1996) · Zbl 0876.68042 |

[43] | Thomsen, B., A theory of higher order communicating systems, Inform. and comput., 116, 38-57, (1995) · Zbl 0823.68061 |

[44] | Victor, B., The fusion calculus: expressiveness and symmetry in mobile processes, (1998), Uppsala University |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.