Complete Axiomatization for the Total Variation Distance of Markov Chains

Research output: Contribution to journalConference article in JournalResearchpeer-review

1 Citation (Scopus)
64 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 =_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
Volume336
Pages (from-to)27-39
Number of pages13
ISSN1571-0661
DOIs
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
http://coalg.org/mfps-calco2017/

Conference

ConferenceMathematical Foundations of Programming Semantics XXXIII
Location Faculty of Mathematics and Physics in Ljubljana
CountrySlovenia
CityLjubljana
Period12/07/201716/07/2017
Internet address

Fingerprint

Total Variation Distance
Axiomatization
Markov processes
Markov chain
Deduction
Distributivity
Approximately equal
Representation Theorem
Prefix
Axiom
Equality
Trace
Equivalence
Metric
Operator

Keywords

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

Cite this

@inproceedings{1dc66891246c4e7790242cf63dc62dd0,
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 =_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).",
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 = "4",
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",

}

Complete Axiomatization for the Total Variation Distance of Markov Chains. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim G.; Mardare, Radu.

In: Electronic Notes in Theoretical Computer Science, Vol. 336, 16.04.2018, p. 27-39.

Research output: Contribution to journalConference article in JournalResearchpeer-review

TY - GEN

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

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

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 - Conference article in Journal

VL - 336

SP - 27

EP - 39

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -