TY - JOUR

T1 - Complete axiomatization for the total variation distance of Markov chains

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim G.

AU - Mardare, Radu

PY - 2018/4/16

Y1 - 2018/4/16

N2 - 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).

AB - 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).

KW - axiomatization

KW - behavioral distances

KW - Markov chains

KW - quantitative deductive systems

UR - http://www.scopus.com/inward/record.url?scp=85045581698&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2018.03.014

DO - 10.1016/j.entcs.2018.03.014

M3 - Article

AN - SCOPUS:85045581698

VL - 336

SP - 27

EP - 39

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -