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