一句话：为有限标记马尔可夫链的互模拟距离给出完备定量公理化，并扩展Kleene式表示定理。
本文研究有限标记马尔可夫链上Desharnais等人提出的互模拟距离，旨在建立完备的定量公理化。作者采用Mardare、Panangaden与Plotkin提出的定量等式逻辑，以有理数ε索引的等式t≡ε s表示“t在误差ε内近似等于s”，并自然扩展Stark与Smolka的概率互模拟等式系统，新增刻画概率分布间Kantorovich距离的公理，从而得到完备的定量演绎系统。该公理化还用于给出Silva等人关于有限标记马尔可夫链的Kleene式表示定理的度量扩展。结果为理论证明，未涉及实现或实验评估。
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS 2016) that uses equality relations $t \equiv_\varepsilon s$ indexed by rationals, expressing that `$t$ is approximately equal to $s$ up to an error $\varepsilon$'. Notably, our quantitative deduction system extends in a natural way the equational system for probabilistic bisimilarity given by Stark and Smolka by introducing an axiom for dealing with the Kantorovich distance between probability distributions. The axiomatization is then used to propose a metric extension of a Kleene's style representation theorem for finite labelled Markov chains, that was proposed (in a more general coalgebraic fashion) by Silva et al. (Inf. Comput. 2011).Comment: Logical Methods in Computer Science
@article{paperbot355,
title = {A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains},
author = {Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Radu Mardare},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:15)2018}
}