×

Tree-functors, determinacy and bisimulations. (English) Zbl 1206.68214

Summary: We study the functorial characterisation of bisimulation-based equivalences over a categorical model of labelled trees. We show that in a setting where all labels are visible, strong bisimilarity can be characterised in terms of enriched functors by relying on the reflection of paths with their factorisations. For an enriched functor \(F\), this notion requires that a path (an internal morphism in our framework) \(\pi \) going from \(F(A)\) to \(C\) corresponds to a path \(p\) going from \(A\) to \(K\), with \(F(K) = C\), such that every possible factorisation of \(\pi \) can be lifted in an appropriate factorisation of \(p\). This last property corresponds to a Conduché property for enriched functors, and a very rigid formulation of it has been used by Lawvere to characterise the determinacy of physical systems. We also consider the setting where some labels are not visible, and provide characterisations for weak and branching bisimilarity. Both equivalences are still characterised in terms of enriched functors that reflect paths with their factorisations: for branching bisimilarity, the property is the same as the one used to characterise strong bisimilarity when all labels are visible; for weak bisimilarity, a weaker form of path factorisation lifting is needed. This fact can be seen as evidence that strong and branching bisimilarity are strictly related and that, unlike weak bisimilarity, they preserve process determinacy in the sense of Milner.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Pavlović, Springer-Verlag Lecture Notes in Computer Science 953 pp 3– (1995) · doi:10.1007/3-540-60164-3_17
[2] DOI: 10.1016/S0304-3975(99)00303-5 · Zbl 0944.68136 · doi:10.1016/S0304-3975(99)00303-5
[3] Milner, Communication and concurrency (1989)
[4] DOI: 10.1016/S0304-3975(01)00023-8 · Zbl 1014.68106 · doi:10.1016/S0304-3975(01)00023-8
[5] van Glabbeeck, Springer-Verlag Lecture Notes in Computer Science 469 pp 309– (1990) · doi:10.1007/3-540-53479-2_13
[6] Kelly, Basic Concepts of Enriched Category Theory (1982) · Zbl 0478.18005
[7] De Nicola, Electronic Notes in Theoretical Computer Science 18 (1998) · doi:10.1016/S1571-0661(05)80249-X
[8] DOI: 10.1016/j.jpaa.2009.05.008 · Zbl 1208.18006 · doi:10.1016/j.jpaa.2009.05.008
[9] De Nicola, Springer-Verlag Lecture Notes in Computer Science 458 pp 152– (1990) · doi:10.1007/BFb0039058
[10] DOI: 10.1017/S0960129599002935 · Zbl 0954.68115 · doi:10.1017/S0960129599002935
[11] Conduché, C. R. Acad. Sci. Paris 275 pp A891– (1972)
[12] Cheng, BRICS Report Series 23 (1995)
[13] Cattani, Springer-Verlag Lecture Notes in Computer Science 1258 pp 106– (1997) · doi:10.1007/BFb0026984
[14] DOI: 10.1017/S0960129599003023 · Zbl 0987.18002 · doi:10.1017/S0960129599003023
[15] Betti, Rend. Ist. Mat. Univ. Trieste 14 pp 41– (1982)
[16] van, Journal of the ACM 43 pp 555– (1989)
[17] DOI: 10.1137/1016026 · Zbl 0288.18005 · doi:10.1137/1016026
[18] Winskel, Handbook of Logic in Computer Science (1995)
[19] Winskel, Springer-Verlag Lecture Notes in Computer Science 354 pp 364– (1988) · doi:10.1007/BFb0013026
[20] Walters, Cahiers de Topologie et Geometrie Diff. 22 pp 283– (1981)
[21] DOI: 10.1016/S0304-3975(00)00056-6 · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6
[22] Park, Springer-Verlag Lecture Notes in Computer Science 104 pp 167– (1981) · doi:10.1007/BFb0017309
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.