Behavioural equivalences are central in the analysis and verification of concurrent systems. They come with a very well-developed meta-theory including logical characterisations, efficient algorithms, game-theoretic perspectives, algebraic characterisations, and generalisations to a wide variety of state-based systems. Two processes or system states are behaviourally equivalent if they are indistinguishable from the point of view of an external observer. Behavioural equivalences have for instance been used for comparing a system with its specification, for the analysis of cryptographic protocols, for the verification of model transformations, for efficient comparison of non-deterministic automata and in programming language semantics.

In recent years, behavioural metrics and quantitative logics specifying quantitative aspects of systems have received considerable attention. Previous approaches are qualitative and address the question "do they match?" whereas metrics address the question "to what degree? how much?". Indeed, a metric measures how far apart two systems are in their behaviour, while a quantitative logic evaluates the degree to which a state satisfies a formula. For quantitative systems such as Markov chains, Markov decision processes and probabilistic automata, a behavioural equivalence is often too strict: small deviations in quantitative information, such as probabilities, can cause two states that intuitively behave very much alike to be inequivalent in a formal sense. Indeed, behavioural equivalence misses robustness under small perturbations in such systems. Metrics and quantitative logics provide a more nuanced approach than qualitative behavioural equivalence.

As behavioural equivalences, behavioural metrics can be characterized via fixpoint equations. In addition there are alternative characterizations of metrics, either via modal logics or via spoiler-duplicator games. The focus of this Dagstuhl Seminar is in particular on quantitative logics, where evaluating a formula on a state does not yield a boolean value, but a (real) number, intuitively indicating to which degree a state satisfies a formula. This is connected to a quantitative Hennessy-Milner property which is supposed to hold for the behavioural distance.

There are various applications in model-checking, differential privacy, hybrid systems and learning. Several challenges in this area have been identified: studying suitable metrics and their corresponding logics, generalizing to the setting of coalgebras by parameterizing the branching type of the system under consideration, developing methods for quantitative algebraic reasoning, and finding efficient methods for computing behavioural metrics.

This Dagstuhl Seminar provided a forum for researchers working in all areas of behavioural metrics and quantitative logics, to discuss the state-of-the-art and further developments, and in particular to address applications in various domains, including machine learning.

The topics discussed at the seminar included all aspects of behavioural metrics and quantitative logics. In particular:

• Various approaches to define behavioural metrics, including characterizations via fixpoint equations, logics and games and their relations.
• Quantitative logics and their expressiveness.
• Methods and theories for quantitative equational reasoning.
• Algorithms for (compositionally) computing behavioural metrics or distinguishing formulas and their efficiency.
• Applications of behavioural metrics and quantitative logics, including – but not limited to – model-checking, differential privacy, hybrid systems and learning.

The seminar programme left room to address the above individual topics, but the main aim was to connect these topics, which previously have been studied by different research groups and published in different venues. Establishing such connections proved to be the main way forward, both to solidify the field and to identify new research problems and opportunities for applications. In particular, a key challenge was to connect recent approaches to quantitative logics, game characterisations, and quantitative equational theories, and to generalise these connections and algorithmic perspectives to enable their application to a wide range of models. We also focused on practical applications and promoted the usefulness of behavioural metrics. The seminar stimulated interactions between more theoretical scientists with researchers working on application-oriented aspects.

We invited four representatives of the different communities to give tutorial talks in order to introduce fundamental concepts and techniques. Specifically, the following four tutorial talks took place on the first day of the seminar:

• Franck van Breugel: Behavioural metrics
• Clemens Kupke: Coalgebras
• Giorgio Bacci: Quantitative equational reasoning
• Pablo Castro: Behavioural metrics for Reinforcement Learning

On Tuesday and Thursday we organized the following working groups in order to discuss more specific topics which were of interest to a substantial part of the participants:

• Generalised Kantorovich-Rubinstein Duality
• Quantitative Algebras/Coalgebras/Modal Logic
• Applications of Behavioural Metrics
• Fixpoints
• Locksteps

The seminar made it possible for many participants to connect and discuss joint collaborations and research projects. The seminar at Dagstuhl was also the opportunity for Matteo Mio, Lutz Schröder, Henning Urbat and Paul Wild to coordinate between the pre-proposal and the full proposal submission for an ANR-DFG project. The full proposal will be submitted in March 2025. This project also involves other applicants from FAU Erlangen-Nürnberg and ENS-Lyon and it aims at furthering our understanding of the theory of quantitative algebras. This topic was the main subject of many talks of this seminar. Further ideas for follow-up events and outreach activities were developed in the wrapup session (for the report on this session see Section 5.6 of the full report).

The organizers would like to thank all the participants and speakers for their inspiring talks and many interesting discussions. Furthermore we would like to acknowledge Florence Clerc who helped to write and prepare this report. A special thanks goes to the Dagstuhl staff who were a great help in organizing this seminar.

Creative Commons BY 4.0

Barbara König, Radu Mardare, Prakash Panangaden, and Jurriaan Rot