Behavioural Metrics and Quantitative Logics (Dagstuhl Seminar 24432)

Abstract

This report documents the program and the outcome of Dagstuhl Seminar "Behavioural Metrics and Quantitative Logics" (24432).
Behavioural metrics and quantitative logics specify quantitative aspects of systems. A metric measures how far apart two systems are in their behaviour while a quantititative 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 of quantitative algebraic reasoning, finding efficient methods for computing behavioural methods. This Dagstuhl Seminar provided a forum to researchers working in this area, to discuss the state-of-the-art and further developments, and in particular address applications in various domains.