Complete Axiomatization for the Total Variation Distance of Markov Chains

Giorgio Bacci*, Giovanni Bacci, Kim G. Larsen, Radu Mardare

*Corresponding author for this work

Research output: Contribution to journalConference article in JournalResearchpeer-review

4 Citations (Scopus)
182 Downloads (Pure)


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 =_e s indexed by rationals, expressing that “t is approximately equal to s up to an error e”. 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).
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Pages (from-to)27-39
Number of pages13
Publication statusPublished - 16 Apr 2018
EventMathematical Foundations of Programming Semantics XXXIII - Faculty of Mathematics and Physics in Ljubljana, Ljubljana, Slovenia
Duration: 12 Jul 201716 Jul 2017


ConferenceMathematical Foundations of Programming Semantics XXXIII
Location Faculty of Mathematics and Physics in Ljubljana
Internet address


  • Axiomatization
  • Behavioral Distances
  • Markov Chains
  • Quantitative Deductive Systems


Dive into the research topics of 'Complete Axiomatization for the Total Variation Distance of Markov Chains'. Together they form a unique fingerprint.

Cite this