License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.27
URN: urn:nbn:de:0030-drops-128394
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12839/
Go to the corresponding LIPIcs Volume Portal

Wild, Paul ; Schröder, Lutz

Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions

pdf-format:
LIPIcs-CONCUR-2020-27.pdf (0.6 MB)

Abstract

Behavioural distances provide a fine-grained measure of equivalence in systems involving quantitative data, such as probabilistic, fuzzy, or metric systems. Like in the classical setting of crisp bisimulation-type equivalences, 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 bisimulations that need not themselves be (pseudo-)metrics, in analogy to classical bisimulations (which need not be equivalence relations). The known instances of 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 non-expansive 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.

BibTeX - Entry

@InProceedings{wild_et_al:LIPIcs:2020:12839,
  author =	{Paul Wild and Lutz Schr{\"o}der},
  title =	{{Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12839},
  URN =		{urn:nbn:de:0030-drops-128394},
  doi =		{10.4230/LIPIcs.CONCUR.2020.27},
  annote =	{Keywords: Modal logic, behavioural distance, coalgebra, bisimulation, lax extension}
}

Keywords: Modal logic, behavioural distance, coalgebra, bisimulation, lax extension
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI