Showing 1–13 of 13 results for author: Wild, P

Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques

Authors: Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, Paul Wild

Abstract: Behavioural distances of transition systems modelled as coalgebras for endofunctors generalize the traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition sys… ▽ More Behavioural distances of transition systems modelled as coalgebras for endofunctors generalize the traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the Kantorovich lifting of a functor on quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition we describe how to lift distributive laws in the case where one of the two functors is polynomial. These results are essential ingredients for adopting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We conclude by illustrating the results of our paper in two case studies. △ Less

Submitted 30 April, 2024; originally announced April 2024.

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, Paul Wild

Abstract: 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… ▽ More 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). △ Less

Submitted 31 January, 2024; v1 submitted 9 October, 2023; originally announced October 2023.

Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Karla Messing

Abstract: Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide wi… ▽ More Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide with language equivalence. Language equivalence can be captured as behavioural equivalence on the determinization, which is obtained via the standard powerset construction. This construction can be lifted to coalgebraic generality, assuming a so-called Eilenberg-Moore distributive law between the functor termining the type of accepted structure (e.g.\ word languages) and a monad capturing the branching type (e.g.\ nondeterministic, weighted, probabilistic). Eilenberg-Moore-style coalgebraic semantics in this sense has been shown to be essentially subsumed by the more general framework of graded semantics, which is centrally based on graded monads. Graded semantics comes with a range of generic results, in particular regarding invariance and, under suitable conditions, expressiveness of dedicated modal logics for a given semantics; notably, these logics are evaluated on the original state space. We show that the instantiation of such graded logics to the case of Eilenberg-Moore-style semantics works extremely smoothly, and yields expressive modal logics in essentially all cases of interest. We additionally parametrize the framework over a quantale of truth values, thus in particular covering both the two-valued notions of equivalence and quantitative ones, i.e. behavioural distances. △ Less

Submitted 26 April, 2024; v1 submitted 27 July, 2023; originally announced July 2023.

MSC Class: 03B45 (Primary) 03B52 (Secondary) ACM Class: F.4.1

Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing

Abstract: 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. We provide a unifying treatment of spectra of behavio… ▽ More 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. We 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 obtain a canonical generic notion of invariant real-valued modal logic, and provide criteria for such logics to be expressive in the sense that logical distance coincides with behavioural distance. We present positive examples based on this criterion, covering both known and new expressiveness results; in particular, we show that expressiveness holds essentially always for Eilenberg-Moore type trace semantics, and we obtain a new expressiveness result for trace semantics of fuzzy transition systems. As a negative result, we show that trace distance on probabilistic metric transition systems does not admit any characteristic real-valued modal logic, even in a more broadly understood sense. △ Less

Submitted 18 October, 2023; v1 submitted 2 June, 2023; originally announced June 2023.

MSC Class: 03B45; 03B52; 68Q85 ACM Class: F.4.1

Quantitative Hennessy-Milner Theorems via Notions of Density

Authors: Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: 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… ▽ More 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. 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-Weierstrass theorem; this allows us to cover, for instance, behavioural ultrametrics. △ Less

Submitted 30 August, 2022; v1 submitted 19 July, 2022; originally announced July 2022.

Kantorovich Functors and Characteristic Logics for Behavioural Distances

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: 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… ▽ More 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. △ Less

Submitted 2 May, 2023; v1 submitted 14 February, 2022; originally announced February 2022.

A Point-free Perspective on Lax extensions and Predicate liftings

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: 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 fundame… ▽ More 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. △ Less

Submitted 7 December, 2023; v1 submitted 23 December, 2021; originally announced December 2021.

Journal ref: Mathematical Structures in Computer Science. 2023:1-30

Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions

Authors: Paul Wild, Lutz Schröder

Abstract: 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… ▽ More 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. △ Less

Submitted 14 June, 2022; v1 submitted 2 July, 2020; originally announced July 2020.

MSC Class: 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 2 (June 15, 2022) lmcs:7351

A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: The fuzzy modality `probably` is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this ob… ▽ More The fuzzy modality `probably` is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that every formula in probabilistic fuzzy first-order logic that is non-expansive wrt. behavioural distance can be approximated by concepts of bounded rank in probabilistic fuzzy description logic. For a modal logic perspective on the same result, see arXiv:1810.04722. △ Less

Submitted 4 June, 2019; v1 submitted 31 May, 2019; originally announced June 2019.

Comments: arXiv admin note: text overlap with arXiv:1810.04722

MSC Class: 60A66; 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

A van Benthem Theorem for Quantitative Probabilistic Modal Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: In probabilistic transition systems, behavioural metrics provide a more fine-grained and stable measure of system equivalence than crisp notions of bisimilarity. They correlate strongly to quantitative probabilistic logics, and in fact the distance induced by a probabilistic modal logic taking values in the real unit interval has been shown to coincide with behavioural distance. For probabilistic… ▽ More In probabilistic transition systems, behavioural metrics provide a more fine-grained and stable measure of system equivalence than crisp notions of bisimilarity. They correlate strongly to quantitative probabilistic logics, and in fact the distance induced by a probabilistic modal logic taking values in the real unit interval has been shown to coincide with behavioural distance. For probabilistic systems, probabilistic modal logic thus plays an analogous role to that of Hennessy-Milner logic on classical labelled transition systems. In the quantitative setting, invariance of modal logic under bisimilarity becomes non-expansivity of formula evaluation w.r.t. behavioural distance. In the present paper, we provide a characterization of the expressive power of probabilistic modal logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that quantitative probabilistic modal logic lies dense in the bisimulation-invariant fragment, in the indicated sense of non-expansive formula evaluation, of quantitative probabilistic first-order logic; more precisely, bisimulation-invariant first-order formulas are approximable by modal formulas of bounded rank. For a description logic perspective on the same result, see arXiv:1906.00784. △ Less

Submitted 4 June, 2019; v1 submitted 10 October, 2018; originally announced October 2018.

MSC Class: 60A66; 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

A van Benthem Theorem for Fuzzy Modal Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exac… ▽ More We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exactly those that can be approximated by fuzzy modal formulas. △ Less

Submitted 5 February, 2018; v1 submitted 1 February, 2018; originally announced February 2018.

MSC Class: 03B45; 03B52; 03B70 ACM Class: F.4.1; I.2.4

A Characterization Theorem for a Modal Description Logic

Authors: Paul Wild, Lutz Schröder

Abstract: Modal description logics feature modalities that capture dependence of knowledge on parameters such as time, place, or the information state of agents. E.g., the logic S5-ALC combines the standard description logic ALC with an S5-modality that can be understood as an epistemic operator or as representing (undirected) change. This logic embeds into a corresponding modal first-order logic S5-FOL. We… ▽ More Modal description logics feature modalities that capture dependence of knowledge on parameters such as time, place, or the information state of agents. E.g., the logic S5-ALC combines the standard description logic ALC with an S5-modality that can be understood as an epistemic operator or as representing (undirected) change. This logic embeds into a corresponding modal first-order logic S5-FOL. We prove a modal characterization theorem for this embedding, in analogy to results by van Benthem and Rosen relating ALC to standard first-order logic: We show that S5-ALC with only local roles is, both over finite and over unrestricted models, precisely the bisimulation invariant fragment of S5-FOL, thus giving an exact description of the expressive power of S5-ALC with only local roles. △ Less

Submitted 23 May, 2017; v1 submitted 17 May, 2017; originally announced May 2017.

MSC Class: 03B45; 03B42; 03B70; 03B10; 03C80 ACM Class: F.4.1; I.2.4

Multi-Organ Cancer Classification and Survival Analysis

Authors: Stefan Bauer, Nicolas Carion, Peter Schüffler, Thomas Fuchs, Peter Wild, Joachim M. Buhmann

Abstract: Accurate and robust cell nuclei classification is the cornerstone for a wider range of tasks in digital and Computational Pathology. However, most machine learning systems require extensive labeling from expert pathologists for each individual problem at hand, with no or limited abilities for knowledge transfer between datasets and organ sites. In this paper we implement and evaluate a variety of… ▽ More Accurate and robust cell nuclei classification is the cornerstone for a wider range of tasks in digital and Computational Pathology. However, most machine learning systems require extensive labeling from expert pathologists for each individual problem at hand, with no or limited abilities for knowledge transfer between datasets and organ sites. In this paper we implement and evaluate a variety of deep neural network models and model ensembles for nuclei classification in renal cell cancer (RCC) and prostate cancer (PCa). We propose a convolutional neural network system based on residual learning which significantly improves over the state-of-the-art in cell nuclei classification. Finally, we show that the combination of tissue types during training increases not only classification accuracy but also overall survival analysis. △ Less

Submitted 2 December, 2016; v1 submitted 2 June, 2016; originally announced June 2016.