Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909089082114048 |
|---|---|
| author | Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla Forster, Jonas Schröder, Lutz Wild, Paul |
| author_facet | Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla Forster, Jonas Schröder, Lutz Wild, Paul |
| contents | We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_05711 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla Forster, Jonas Schröder, Lutz Wild, Paul Logic in Computer Science We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances). |
| title | Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2310.05711 |