Complete axiomatization for the total variation distance of Markov chains

Giorgio Bacci; Giovanni Bacci; Kim G. Larsen; Radu Mardare

doi:10.1016/j.entcs.2018.03.014

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 journal › Article › peer-review

8 Citations (Scopus)

18 Downloads (Pure)

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

Original language	English
Pages (from-to)	27-39
Number of pages	13
Journal	Electronic Notes in Theoretical Computer Science
Volume	336
DOIs	https://doi.org/10.1016/j.entcs.2018.03.014
Publication status	Published - 16 Apr 2018
Event	33rd Conference on the Mathematical Foundations of Programming Semantics - Ljubljana, Slovenia Duration: 12 Jun 2017 → 15 Jun 2017

Funding

This work has been supported by the EU 7th Framework Programme (FP7/2007-13) under Grants Agreement nr.318490 (SENSATION), nr.601148 (CASSTING), the Sino-Danish Basic Research Center IDEA4CPS funded by Danish National Research Foundation and National Science Foundation China, the ASAP Project (4181-00360) funded by the Danish Council for Independent Research, the ERC Advanced Grant LASSO, and the Innovation Fund Denmark center DiCyPS.

Keywords

axiomatization
behavioral distances
Markov chains
quantitative deductive systems

Access to Document

10.1016/j.entcs.2018.03.014Licence: CC BY-NC-ND 4.0

Bacci-etal-ENTCS-2018-Complete-axiomatization-for-the-total-variation-distance-of-Markov-chainsFinal published version, 329 KBLicence: CC BY-NC-ND 4.0

Cite this

@article{81dd272c048e4053b3432a34d71bed0b,

title = "Complete axiomatization for the total variation distance of Markov chains",

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).",

keywords = "axiomatization, behavioral distances, Markov chains, quantitative deductive systems",

author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim G.} and Radu Mardare",

year = "2018",

month = apr,

day = "16",

doi = "10.1016/j.entcs.2018.03.014",

language = "English",

volume = "336",

pages = "27--39",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

note = "33rd Conference on the Mathematical Foundations of Programming Semantics, MFPS 2017 ; Conference date: 12-06-2017 Through 15-06-2017",

}

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

U2 - 10.1016/j.entcs.2018.03.014

DO - 10.1016/j.entcs.2018.03.014

M3 - Article

AN - SCOPUS:85045581698

SN - 1571-0661

VL - 336

SP - 27

EP - 39

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 33rd Conference on the Mathematical Foundations of Programming Semantics

Y2 - 12 June 2017 through 15 June 2017

ER -

Complete axiomatization for the total variation distance of Markov chains

Abstract

Funding

Keywords

Access to Document

Fingerprint

Cite this