Behavioural Metrics and Quantitative Logics

Drawing (a multiset of) coloured balls from an urn is one of the most basic models in discrete probability theory. Three modes of drawing are commonly distinguished: multinomial (draw-replace), hypergeometric (draw-delete), and Polya (draw-add). These drawing operations are represented as maps from urns to distributions over multisets of draws. The set of urns is a metric space via the Wasserstein distance. The set of distributions over draws is also a metric space, using Wasserstein-over-Wasserstein. It is shown that these three draw operations are all isometries, that is, they exactly preserve the Wasserstein distances. Further, drawing is studied in the limit, both for large urns and for large draws. First it is shown that, as the urn size increases, the Wasserstein distances go to zero between hypergeometric and multinomial draws, and also between Pólya and multinomial draws. Second, it is shown that, as the draw size increases, the Wasserstein distance goes to zero (in probability) between an urn and (normalised) multinomial draws from the urn. These results are known, but here, they are formulated in a novel manner as limits of Wasserstein distances. We call these two limit results the law of large urns and the law of large draws.

We present the main principles of Lawvere Logic, a logic interpreted on top of the semiring of extended positive reals taken with reverse order. This realizes and extends some of the ideas of Lawvere for developing the theory of metric spaces. Lawvere logics are proposed both as a way to extend the quantitative equational logics, and as a way of approaching approximation theories.

I will present some recent generalisations of the theory of quantitative algebras, originally introduced by Mardare Panangaden Plotkin in a LICS 2016 paper, which can accomodate quantitative algebras whose distance and operations are not restricted to be metrics and nonexpansive maps, respectively.

Probabilistic bisimilarity distances measure the similarity of behaviour of states of a labelled Markov chain. The smaller the distance between two states, the more alike they behave. Their distance is zero if and only if they are probabilistic bisimilar. Recently, algorithms have been developed that can compute probabilistic bisimilarity distances for labelled Markov chains with thousands of states within seconds. However, say we compute that the distance of two states is 0.125. How does one explain that 0.125 captures the similarity of their behaviour?

In this talk, we discuss two approaches to explainability: a logical one and a game-theoretic one. In the logical approach, which is joint work with Amgad Rady, we address the question of explainability by returning to the definition of probabilistic bisimilarity distances proposed by Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden more than two decades ago. We use a slight variation of their logic to construct for each pair of states a sequence of formulas that explains the probabilistic bisimilarity distance of the states. We have developed and implemented an algorithm that computes those formulas and each formula can be computed in polynomial time.

The game-theoretic approach is joint work with Anto Nanah Ji, Emily Vlasman, and James Worrell. We demonstrate that the probabilistic bisimilarity distances can be explained by a policy of a game. We start from a characterization of probabilistic bisimilarity distances provided in joint work with Di Chen and James Worrell. We identify properties of policies that make them suitable for explaining the probabilistic bisimilarity distances and present algorithms to generate policies with those properties.

Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one is commonly led to consider least fixpoints of (higher-dimensional) functions over the non-negative reals. We show how to approximate the least fixpoint of such functions, focusing on the case in which they are not known precisely, but represented by a sequence of approximating functions that converge to them. We concentrate on monotone and non-expansive functions, for which uniqueness of fixpoints is not guaranteed and standard fixpoint iteration schemes might get stuck at a fixpoint that is not the least. Our main contribution is the identification of an iteration scheme, a variation of Mann iteration with a dampening factor, which, under suitable conditions, is shown to guarantee convergence to the least fixpoint of the function of interest. We then argue that these results are relevant in the context of model-based reinforcement learning for Markov decision processes (MDPs), showing that the proposed iteration scheme instantiates to MDPs and allows us to derive convergence to the optimal expected return. More generally, we show that our results can be used to iterate to the least fixpoint almost surely for systems where the function of interest can be approximated with given probabilistic error bounds, as it happens for probabilistic systems, which can be explored via sampling.

Behavioural metrics provide a robust measure of the behaviour of 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, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; as a salient negative examples, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities, in a well-delineated but broadly understood sense. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads (Milius, Schröder, Pattinson, CALCO 2015), 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 $\mathrm{𝐌𝐞𝐭}$ of metric spaces, generalizing previous systems aimed at presenting plain monads on $\mathrm{𝐌𝐞𝐭}$ (Mardare, Panangaden, Plotkin, LICS 2016). Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance, phrased in terms of a separation property that depends both on the modalities and on the propositional operators of the logic. We apply this criterion to a number of case studies, notably including a new characteristic modal logic for trace distance in fuzzy metric transition systems. In a concluding discussion, we give an outlook on generic game characterizations of behavioural metrics and indeed of more general behavioural conformances, such as behavioural preorders or bisimulation topologies.

Deterministic automata have been traditionally studied from the point of view of language equivalence, but another perspective is given by the canonical notion of shortest-distinguishing word distance quantifying the difference of states. Intuitively, the longer the word needed to observe a difference between two states, then the closer behaviour is. In this talk, I discuss a sound and complete axiomatisation of shortest-distinguishing-word distance between regular languages. The axiomatisation relies on a recently developed analogue of equational logic for approximate, quantitative reasoning, allowing to manipulate rational-indexed judgements of the form $e{=}_{ϵ}f$, meaning term $e$ is approximately equal to term $f$ within the error margin of $ϵ$. The completeness argument draws techniques from order theory and Banach spaces to simplify the calculation of behavioural distance to the point it can be then mimicked by axiomatic reasoning.

Contextual equivalence considers two higher-order programs as equivalent when they behave the same in any given context, and contexts are modelled as programs written in the same language, making this definition self-contained. In a probabilistic setting, this definition can be made quantitative in a natural way: the distance between two programs M and N is defined as the supremum at the difference that a context can observe in the behaviour of M and N. However, it has been shown by Crubillé and Dal Lago that when all programs terminate with probability 1, this definition of contextual distance actually leads to a trivial pseudometric: two programs are either equivalent, or they are as far away as possible of each other. The original proof of this fact used techniques from real analysis with Bernstein’s theorem as a pivotal tool. In this talk, I presented a new proof that hilights the deep connection of this trivialisation result with the law of large numbers.

Higher-order coalgebras are a convenient abstract setting for modelling higher-order languages and their operational semantics. In this talk, I introduce a fibrational approach to reasoning about congruence properties of higher-order coalgebras. It uniformly applies to various notions and applicative bisimilarity and applicative distances known in the literature, as well as to new settings such as higher-order languages combining nondeterministic and probabilistic effects.

A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ExTh(R)-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies.

In this talk, I will be looking at extending the notion of bismulation and bisimulation metrics from discrete-time to continuous-time. The whole discrete-time approach relies entirely on the step-based dynamics: the process jumps from state to state. What we mean by continuous-time is that processes evolve continuously through time, such as Brownian motion or involve jumps or both.

I will first recall some previous work on how to extend the notion of bisimulation to continuous-time by considering trajectories and I will discuss the limits of this approach.

I will then generalize the concept of bisimulation metric in order to metrize the behaviour of continuous-time processes. Similarly to what is done for discrete-time systems, we follow two approaches and show that they coincide: as a fixpoint of a functional and through a real-valued logic.

Polytopal stochastic games are an extension of two-player, zero-sum, turn-based stochastic games. In these games the uncertainty over the probability distributions is captured via linear (in)equalities whose space of solutions forms a polytope. The idea has its root in a previous work (Castro et al. EXPRESS/SOS 2023) that explores a distance to quantify robustness of fault-tolerant algorithms. Such distance is the value of a total accumulative reward objective in a stochastic game where one of the players needs to choose transitions from a polytope of distributions. Polytopal stochastic games extend this idea so that both players can choose distribution from a finite set of polytopes of distributions. In the presentation I discuss reachability and different reward objectives and present results of determinacy, decidability and complexity. This presentation is based on a joint work with Pablo Castro (UNRC, CONICET) that has been recently submitted for publication.

The most studied and accepted pseudo metric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results. With all these seals of approval, it has imposed itself as the one to study.

Other notions of pseudometrics have been proposed, one of them (epsilon-distance) based on epsilon-bisimulation. Its advantages over the Kantorovich distance are that it is intuitively easier to understand, it relates systems that have close probabilites even if these differences can imply very different behavior in the long run. For example an imperfect implementation can be considered close to its specification. Finally, it it is easier to compute.

However, this approximate equivalence has only been defined on Markov chains in a structural way. We show that epsilon-distance is also the greatest fixpoint of a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokorov distance.

Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity.

Today, I’ll talk about some of our recent work on NumFuzz, a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Subject to certain restrictions, our type inference procedure derives sound relative error bounds for programs that are several orders of magnitude larger than previously possible, while deriving relative error bounds that are several orders of magnitude more precise than prior work.

We introduce backward dissimilarity (BD) for discrete-time linear dynamical systems (LDS), which relaxes existing notions of bisimulations by allowing for approximate comparisons. BD is an invariant property stating that the difference along the evolution of the dynamics governing two state variables is bounded by a constant, which we call dissimilarity. We demonstrate the applicability of BD in a simple case study and showcase its use concerning: (i) robust model comparison; (ii) approximate model reduction; and (iii) approximate data recovery. Our main technical contribution is a policy-iteration algorithm to compute BDs. Using a prototype implementation, we apply it to benchmarks from network science and discrete-time Markov chains and compare it against a related notion of bisimulation for linear control systems.