In recent years, behavioural metrics and quantitative logics specifying quantitative aspects of systems have received considerable attention. 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. They are often intimately connected via a Hennessy-Milner theorem stating that the distance induced by a quantitative logic coincides with 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 aims at providing 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 to be discussed at the seminar therefore include 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.
• All applications of behavioural metrics and quantitative logics, including – but not limited to – model-checking, differential privacy, hybrid systems and learning.

The seminar programme leaves room to address the above individual topics, but the main aim is to connect these topics, which have been studied by different research groups and published in different venues in recent years. We believe that establishing such connections are the main way forward, both to solidify the field and to identify new research problems and opportunities for applications. In particular, a key challenge is 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. Moreover, we believe that work on practical applications is still underrepresented, despite clear indications of the usefulness of behavioural metrics. Hence, we plan to stimulate interactions between more theoretical scientists with researchers working on application-oriented aspects.

The seminar will include tutorials and will partially be organized as a hands-on workshop, encouraging interaction and discussions via breakout sessions and panel discussions.

Creative Commons BY 4.0

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