Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-19T11:10:44.920Z Has data issue: false hasContentIssue false
  • English
  • Français

Tree-functors, determinacy and bisimulations

Published online by Cambridge University Press:  04 February 2010

ROCCO DE NICOLA ,
DANIELE GORLA  and
ANNA LABELLA
ROCCO DE NICOLA
Affiliation:
Dip. di Sistemi ed Informatica – Univ. di Firenze, Viale Morgagni 65, 50134 Firenze, Italy Email: [email protected]
DANIELE GORLA
Affiliation:
Dip. di Informatica – Univ. di Roma ‘La Sapienza’, Via Salaria 113, 00198 Roma, Italy Email: [email protected], [email protected]
ANNA LABELLA
Affiliation:
Dip. di Informatica – Univ. di Roma ‘La Sapienza’, Via Salaria 113, 00198 Roma, Italy Email: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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) π 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 π 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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 20 , Issue 3 , June 2010 , pp. 319 - 358
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Arbib, M. A. and Manes, E. G. (1974) Machines in a category: an expository introduction. SIAM Review 16 (2)163–192.Google Scholar
Betti, R. and Kasangian, S. (1982) A quasi-universal realization of automata. Rend. Ist. Mat. Univ. Trieste 14 41–48.Google Scholar
Bunge, M. and Fiore, M. P. (2000) Unique factorisation lifting functors and categories of linearly-controlled processes. Mathematical Structures in Computer Science 10 (2)137–163.Google Scholar
Cattani, G. L. and Winskel, G. (1997) Preshaf models for concurrency. Proc. of CSL ‘96. Springer-Verlag Lecture Notes in Computer Science 1258 106–126.Google Scholar
Cheng, A. and Nielsen, M. (1995) Open Maps (at) Work. BRICS Report Series 23.Google Scholar
Conduché, F. (1972) Au sujet de l'existence d'adjoints à droîte aux foncteurs ‘image reciproque’ dans la catégorie des catégories. C. R. Acad. Sci. Paris 275 A891–894.Google Scholar
De Nicola, R., Montanari, U. and Vaandrager, F. (1990) Back and forth bisimulations. In: Proc. of CONCUR'90. Springer-Verlag Lecture Notes in Computer Science 458 152–165.Google Scholar
De Nicola, R. and Labella, A. (1998) Tree Morphisms and Bisimulations. In: Proc. of MFCS'98 Workshop on Concurrency. Electronic Notes in Theoretical Computer Science 18.Google Scholar
van Glabbeeck, R. and Goltz, U. (1990) Equivalences and refinement. In: Semantics of Systems of Concurrent Processes. Springer-Verlag Lecture Notes in Computer Science 469 309–333.Google Scholar
vanGlabbeek, R. Glabbeek, R. and Weijland, W. (1989) Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43 (3)555–600.Google Scholar
Joyal, A., Nielsen, M. and Winskel, G. (1993) Bisimulations and Open Maps. In: Proc. of LICS, IEEE 418–427.CrossRefGoogle Scholar
Kasangian, S. and Labella, A. (1999) Observational trees as models for concurrency. Mathematical Structures in Computer Science 9 687–718.CrossRefGoogle Scholar
Kasangian, S. and Labella, A. (2010) Conduché property and Tree-based categories. Journal of Pure and Applied Algebra 214 221–235.Google Scholar
Kelly, G. (1982) Basic Concepts of Enriched Category Theory, Cambridge University Press.Google Scholar
Lasota, S. (2002) Coalgebra morphisms subsume open maps. Theoretical Computer Science 280 123–135.Google Scholar
Lawvere, F. W. (1986) State categories and response functors (unpublished manuscript).Google Scholar
Milner, R. (1989) Communication and concurrency, Prentice Hall International.Google Scholar
Park, D. (1981) Concurrency and automata on infinite sequences. In: Proc. of Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 104 167–183.Google Scholar
Pavlović, D. (1995) Convenient Category of Processes and Simulations 1: Modulo Strong Bisimilarity. In: Proc. of Category Theory and Computer Science. Springer-Verlag Lecture Notes in Computer Science 953 3–23.Google Scholar
Pavlović, D. (1996) Convenient categories of asynchronous processes and simulations II. In: Edalat, A. (ed.) Theory and Formal Methods of Computing '96, World Scientific 156–167.Google Scholar
Roggenbach, M. and Majster-Cederbaum, M. (2000) Towards a unified view of bisimulation: a comparative study. Theoretical Computer Science 238 81–130.Google Scholar
Rutten, J. (2000) Universal coalgebra – a theory of systems. Theoretical Computer Science 249 (1)3–80.Google Scholar
Walters, R. (1981) Sheaves and Cauchy-complete categories. Cahiers de Topologie et Geometrie Diff. 22 283–286.Google Scholar
Winskel, G. (1988) An introduction to event structures. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag Lecture Notes in Computer Science 354 364–397.Google Scholar
Winskel, G. and Nielsen, M. (1995) Models for Concurrency. In: Abramsky, S., Gabbay, D. and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science, Oxford University Press.Google Scholar