A point-free perspective on lax extensions and predicate liftings - Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Mathematical Structures in Computer Science, 2023)
Lax extensions of set functors play a key role in various areas, including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result.
CRIS-Team Scopus Importer:2023-12-15
Keywords: coalgebraic modal logic; Kantorovich extension; Lax extension; Moss lifting

Duality theory for enriched Priestley spaces - Hofmann, Dirk; Nora, Pedro (Journal of Pure and Applied Algebra, 2023)
The term Stone-type duality often refers to a dual equivalence between a category of lattices or other partially ordered structures on one side and a category of topological structures on the other. This paper is part of a larger endeavour that aims to extend a web of Stone-type dualities from ordered to metric structures and, more generally, to quantale-enriched categories. In particular, we improve our previous work and show how certain duality results for categories of [0,1]-enriched Priestley spaces and [0,1]-enriched relations can be restricted to functions. In a broader context, we investigate the category of quantale-enriched Priestley spaces and continuous functors, with emphasis on those properties which identify the algebraic nature of the dual of this category.
CRIS-Team Scopus Importer:2022-09-30
Keywords: Metric space; Priestley space; Quantale-enriched category; Quasivariety; Stone duality; Variety

Kantorovich Functors and Characteristic Logics for Behavioural Distances - Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023)
Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo)metrics, and probabilistic (pseudo)metrics. Coalgebraic behavioural distances have been based either on liftings of Set -functors to categories of metric spaces, or on lax extensions of Set -functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic.
CRIS-Team Scopus Importer:2023-08-04

Quantitative Hennessy-Milner Theorems via Notions of Density - Forster, Jonas; Goncharov, Sergey; Hofmann, Dirk; Nora, Pedro; Schröder, Lutz; Wild, Paul (Leibniz International Proceedings in Informatics, LIPIcs, 2023)
The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g. in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance of such a general result. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstraß theorem; this allows us to cover, for instance, behavioural ultrametrics.
CRIS-Team Scopus Importer:2023-03-03
Keywords: Behavioural distances; characteristic modal logics; coalgebra; density; Hennessy-Milner theorems; quantale-enriched categories; Stone-Weierstraß theorems