| Summary: | In this paper we propose a complete axiomatization of the bisimilarity
distance of Desharnais et al. for the class of finite labelled Markov chains.
Our axiomatization is given in the style of a quantitative extension of
equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS
2016) that uses equality relations $t \equiv_\varepsilon s$ indexed by
rationals, expressing that `$t$ is approximately equal to $s$ up to an error
$\varepsilon$'. Notably, our quantitative deduction system extends in a natural
way the equational system for probabilistic bisimilarity given by Stark and
Smolka by introducing an axiom for dealing with the Kantorovich distance
between probability distributions. The axiomatization is then used to propose a
metric extension of a Kleene's style representation theorem for finite labelled
Markov chains, that was proposed (in a more general coalgebraic fashion) by
Silva et al. (Inf. Comput. 2011).
|
|---|