Complete axiomatization for the bisimilarity distance on Markov chains

Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim G. and Mardare, Radu; Desharnais, Josee and Jagadeesan, Radha, eds. (2016) Complete axiomatization for the bisimilarity distance on Markov chains. In: 27th International Conference on Concurrency Theory, CONCUR 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, CAN. ISBN 9783959770170 (https://doi.org/10.4230/LIPIcs.CONCUR.2016.21)

[thumbnail of Bacci-etal-CONCUR2016-Complete-axiomatization-bisimilarity-distance-Markov-chains]
Preview
 Text. Filename: Bacci_etal_CONCUR2016_Complete_axiomatization_bisimilarity_distance_Markov_chains.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (601kB)| Preview

Abstract

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'16) that uses equality relations t ϵ s indexed by rationals, expressing that "t is approximately equal to s up to an error ϵ. Notably, our quantitative deductive 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.

CORE (COnnecting REpositories)