摘要：In this paper we propose a complete axiomatization of the bisimilaritydistance of Desharnais et al. for the class of finite labelled Markov chains.Our axiomatization is given in the style of a quantitative extension ofequational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS2016) that uses equality relations $t \equiv_\varepsilon s$ indexed byrationals, expressing that `$t$ is approximately equal to $s$ up to an error$\varepsilon$'. Notably, our quantitative deduction system extends in a naturalway the equational system for probabilistic bisimilarity given by Stark andSmolka by introducing an axiom for dealing with the Kantorovich distancebetween probability distributions. The axiomatization is then used to propose ametric extension of a Kleene's style representation theorem for finite labelledMarkov chains, that was proposed (in a more general coalgebraic fashion) bySilva et al. (Inf. Comput. 2011).
