-
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.
-
NetKet 3: Machine Learning Toolbox for Many-Body Quantum Systems
Authors:
Filippo Vicentini,
Damian Hofmann,
Attila Szabó,
Dian Wu,
Christopher Roth,
Clemens Giuliani,
Gabriel Pescia,
Jannes Nys,
Vladimir Vargas-Calderon,
Nikita Astrakhantsev,
Giuseppe Carleo
Abstract:
We introduce version 3 of NetKet, the machine learning toolbox for many-body quantum physics. NetKet is built around neural-network quantum states and provides efficient algorithms for their evaluation and optimization. This new version is built on top of JAX, a differentiable programming and accelerated linear algebra framework for the Python programming language. The most significant new feature…
▽ More
We introduce version 3 of NetKet, the machine learning toolbox for many-body quantum physics. NetKet is built around neural-network quantum states and provides efficient algorithms for their evaluation and optimization. This new version is built on top of JAX, a differentiable programming and accelerated linear algebra framework for the Python programming language. The most significant new feature is the possibility to define arbitrary neural network ansätze in pure Python code using the concise notation of machine-learning frameworks, which allows for just-in-time compilation as well as the implicit generation of gradients thanks to automatic differentiation. NetKet 3 also comes with support for GPU and TPU accelerators, advanced support for discrete symmetry groups, chunking to scale up to thousands of degrees of freedom, drivers for quantum dynamics applications, and improved modularity, allowing users to use only parts of the toolbox as a foundation for their own code.
△ Less
Submitted 18 August, 2022; v1 submitted 20 December, 2021;
originally announced December 2021.
-
Limits in Categories of Vietoris Coalgebras
Authors:
Dirk Hofmann,
Renato Neves,
Pedro Nora
Abstract:
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. Wh…
▽ More
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions the resulting categories of coalgebras are even complete. As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability, and behaviour.
△ Less
Submitted 6 February, 2017; v1 submitted 10 December, 2016;
originally announced December 2016.
-
Continuity as a computational effect
Authors:
Renato Neves,
Luis S. Barbosa,
Dirk Hofmann,
Manuel A. Martins
Abstract:
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of contin…
▽ More
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of continuous behaviour as (yet another) computational effect. This paper introduces such an encoding through a monad which, in the compositional development of hybrid systems, may play a role similar to the one played by the 1+, powerset, and distribution monads in the characterisation of partial, non deterministic and probabilistic components, respectively. This monad and its Kleisli category provide a setting in which the effects of continuity over (different forms of) composition can be suitably studied.
△ Less
Submitted 1 August, 2016; v1 submitted 12 July, 2015;
originally announced July 2015.
-
On a coalgebraic view on Logic
Authors:
Dirk Hofmann,
Manuel A. Martins
Abstract:
In this paper we present methods of transition from one perspective on logic to others, and apply this in particular to obtain a coalgebraic presentation of logic. The central ingredient in this process is to view consequence relations as morphisms in a category.
In this paper we present methods of transition from one perspective on logic to others, and apply this in particular to obtain a coalgebraic presentation of logic. The central ingredient in this process is to view consequence relations as morphisms in a category.
△ Less
Submitted 4 February, 2012;
originally announced February 2012.
-
Approximation in quantale-enriched categories
Authors:
Dirk Hofmann,
Pawel Waszkiewicz
Abstract:
Our work is a fundamental study of the notion of approximation in V-categories and in (U,V)-categories, for a quantale V and the ultrafilter monad U. We introduce auxiliary, approximating and Scott-continuous distributors, the way-below distributor, and continuity of V- and (U,V)-categories. We fully characterize continuous V-categories (resp. (U,V)-categories) among all cocomplete V-categories (r…
▽ More
Our work is a fundamental study of the notion of approximation in V-categories and in (U,V)-categories, for a quantale V and the ultrafilter monad U. We introduce auxiliary, approximating and Scott-continuous distributors, the way-below distributor, and continuity of V- and (U,V)-categories. We fully characterize continuous V-categories (resp. (U,V)-categories) among all cocomplete V-categories (resp. (U,V)-categories) in the same ways as continuous domains are characterized among all dcpos. By varying the choice of the quantale V and the notion of ideals, and by further allowing the ultrafilter monad to act on the quantale, we obtain a flexible theory of continuity that applies to partial orders and to metric and topological spaces. We demonstrate on examples that our theory unifies some major approaches to quantitative domain theory.
△ Less
Submitted 13 April, 2010;
originally announced April 2010.
