Explainability: from Behavioural Equivalences to Behavioural Distances

8^th June 2023, 13:00 6th Floor Conference Room 605, EEE
Prof. Franck van Breugel
York University, Toronto

Abstract

Behavioural equivalences capture which states of a model behave the same. To explain why states behave differently, logics have been used. We review behavioural equivalences for three models: bisimilarity for labelled transition systems and probabilistic bisimilarity for labelled Markov chains and for probabilistic automata. Behavioural equivalences are not robust as minuscule perturbations to the model may change which states are considered equivalent. Distances, which measure the similarity of behaviour by mapping each pair of the states to a real number in the interval [0, 1], provide a robust alternative. The smaller the distance, the more alike the states behave. Distance zero captures behavioural equivalence. To explain behavioural distances, real-valued logics are used. The interpretation of a formula of the logic in a state of the models is a real number that can be thought of as the probability that the formula is satisfied in the state. It is shown how a real-valued logic can be used to explain probabilistic bisimilarity distances for labelled Markov chains.