Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions
In systems involving quantitative data, such as probabilistic, fuzzy, or metric systems, behavioural distances provide a more fine-grained comparison of states than two-valued notions of behavioural equivalence or behaviour inclusion. Like in the two-valued case, the wide variation found in system t...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7351/pdf |
| _version_ | 1827322735022309376 |
|---|---|
| author | Paul Wild Lutz Schröder |
| author_facet | Paul Wild Lutz Schröder |
| author_sort | Paul Wild |
| collection | DOAJ |
| description | In systems involving quantitative data, such as probabilistic, fuzzy, or
metric systems, behavioural distances provide a more fine-grained comparison of
states than two-valued notions of behavioural equivalence or behaviour
inclusion. Like in the two-valued case, the wide variation found in system
types creates a need for generic methods that apply to many system types at
once. Approaches of this kind are emerging within the paradigm of universal
coalgebra, based either on lifting pseudometrics along set functors or on
lifting general real-valued (fuzzy) relations along functors by means of fuzzy
lax extensions. An immediate benefit of the latter is that they allow bounding
behavioural distance by means of fuzzy (bi-)simulations that need not
themselves be hemi- or pseudometrics; this is analogous to classical
simulations and bisimulations, which need not be preorders or equivalence
relations, respectively. The known generic pseudometric liftings, specifically
the generic Kantorovich and Wasserstein liftings, both can be extended to yield
fuzzy lax extensions, using the fact that both are effectively given by a
choice of quantitative modalities. Our central result then shows that in fact
all fuzzy lax extensions are Kantorovich extensions for a suitable set of
quantitative modalities, the so-called Moss modalities. For nonexpansive fuzzy
lax extensions, this allows for the extraction of quantitative modal logics
that characterize behavioural distance, i.e. satisfy a quantitative version of
the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a
quantitative version of Moss' coalgebraic logic. All our results explicitly
hold also for asymmetric distances (hemimetrics), i.e. notions of quantitative
simulation. |
| first_indexed | 2024-04-25T01:33:32Z |
| format | Article |
| id | doaj.art-8acd786f9fe946ffb8d36916978cc1a6 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:32Z |
| publishDate | 2022-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-8acd786f9fe946ffb8d36916978cc1a62024-03-08T10:38:41ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-06-01Volume 18, Issue 210.46298/lmcs-18(2:19)20227351Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax ExtensionsPaul WildLutz SchröderIn systems involving quantitative data, such as probabilistic, fuzzy, or metric systems, behavioural distances provide a more fine-grained comparison of states than two-valued notions of behavioural equivalence or behaviour inclusion. Like in the two-valued case, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy (bi-)simulations that need not themselves be hemi- or pseudometrics; this is analogous to classical simulations and bisimulations, which need not be preorders or equivalence relations, respectively. The known generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For nonexpansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic. All our results explicitly hold also for asymmetric distances (hemimetrics), i.e. notions of quantitative simulation.https://lmcs.episciences.org/7351/pdfcomputer science - logic in computer science68q85, 03b45, 03b52f.4.1i.2.4 |
| spellingShingle | Paul Wild Lutz Schröder Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions Logical Methods in Computer Science computer science - logic in computer science 68q85, 03b45, 03b52 f.4.1 i.2.4 |
| title | Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions |
| title_full | Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions |
| title_fullStr | Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions |
| title_full_unstemmed | Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions |
| title_short | Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions |
| title_sort | characteristic logics for behavioural hemimetrics via fuzzy lax extensions |
| topic | computer science - logic in computer science 68q85, 03b45, 03b52 f.4.1 i.2.4 |
| url | https://lmcs.episciences.org/7351/pdf |
| work_keys_str_mv | AT paulwild characteristiclogicsforbehaviouralhemimetricsviafuzzylaxextensions AT lutzschroder characteristiclogicsforbehaviouralhemimetricsviafuzzylaxextensions |