Relational Connectors and Heterogeneous Bisimulations
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917914289897472 |
|---|---|
| author | Nora, Pedro Rot, Jurriaan Schröder, Lutz Wild, Paul |
| author_facet | Nora, Pedro Rot, Jurriaan Schröder, Lutz Wild, Paul |
| contents | While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_14460 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Relational Connectors and Heterogeneous Bisimulations Nora, Pedro Rot, Jurriaan Schröder, Lutz Wild, Paul Logic in Computer Science 68Q85, 03B70, 03B45, 18A25 F.3.1; F.4.1 While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances. |
| title | Relational Connectors and Heterogeneous Bisimulations |
| topic | Logic in Computer Science 68Q85, 03B70, 03B45, 18A25 F.3.1; F.4.1 |
| url | https://arxiv.org/abs/2410.14460 |