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'16) that uses equality relations t =_e s indexed by rationals, expressing that "t is approximately equal to s up to an error e". Notably, our quantitative deductive 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.
@InProceedings{bacci_et_al:LIPIcs.CONCUR.2016.21, author = {Bacci, Giorgio and Bacci, Giovanni and G. Larsen, Kim and Mardare, Radu}, title = {{Complete Axiomatization for the Bisimilarity Distance on Markov Chains}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {21:1--21:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.21}, URN = {urn:nbn:de:0030-drops-61569}, doi = {10.4230/LIPIcs.CONCUR.2016.21}, annote = {Keywords: Markov chains, Behavioral distances, Axiomatization} }
Feedback for Dagstuhl Publishing