Complete axiomatization for the total variation distance of Markov chains

Tools

Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim G. and Mardare, Radu (2018) Complete axiomatization for the total variation distance of Markov chains. Electronic Notes in Theoretical Computer Science, 336. pp. 27-39. ISSN 1571-0661 (https://doi.org/10.1016/j.entcs.2018.03.014)

[thumbnail of Bacci-etal-ENTCS-2018-Complete-axiomatization-for-the-total-variation-distance-of-Markov-chains]
Preview
 Text. Filename: Bacci_etal_ENTCS_2018_Complete_axiomatization_for_the_total_variation_distance_of_Markov_chains.pdf
Final Published Version
License: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 logo
Download (337kB)| Preview

Abstract

We propose a complete axiomatization for the total variation distance of finite labelled Markov chains. Our axiomatization is given in the form of a quantitative deduction system, a framework recently proposed by Mardare, Panangaden, and Plotkin (LICS 2016) to extend classical equational deduction systems by means of inferences of equality relations t≡εs indexed by rationals, expressing that “t is approximately equal to s up to an error ε”. Notably, the quantitative equational system is obtained by extending our previous axiomatization (CONCUR 2016) for the probabilistic bisimilarity distance with a distributivity axiom for the prefix operator over the probabilistic choice inspired by Rabinovich's (MFPS 1983). Finally, we propose a metric extension to the Kleene-style representation theorem for finite labelled Markov chains w.r.t. trace equivalence due to Silva and Sokolova (MFPS 2011).

CORE (COnnecting REpositories)