Quantitative Graded Semantics and Spectra of Behavioural Metrics
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909465830227968 |
|---|---|
| author | Forster, Jonas Schröder, Lutz Wild, Paul Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla |
| author_facet | Forster, Jonas Schröder, Lutz Wild, Paul Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla |
| contents | Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_01487 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Quantitative Graded Semantics and Spectra of Behavioural Metrics Forster, Jonas Schröder, Lutz Wild, Paul Beohar, Harsh Gurke, Sebastian König, Barbara Messing, Karla Logic in Computer Science 03B45, 03B52, 68Q85 F.4.1 Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems. |
| title | Quantitative Graded Semantics and Spectra of Behavioural Metrics |
| topic | Logic in Computer Science 03B45, 03B52, 68Q85 F.4.1 |
| url | https://arxiv.org/abs/2306.01487 |