3 years ago

# A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains.

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

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). Publisher URL: http://arxiv.org/abs/1702.02528 DOI: arXiv:1702.02528v4 You might also like Discover & Discuss Important Research Keeping up-to-date with research can feel impossible, with papers being published faster than you'll ever be able to read them. That's where Researcher comes in: we're simplifying discovery and making important discussions happen. With over 19,000 sources, including peer-reviewed journals, preprints, blogs, universities, podcasts and Live events across 10 research areas, you'll never miss what's important to you. It's like social media, but better. Oh, and we should mention - it's free. Researcher displays publicly available abstracts and doesn’t host any full article content. If the content is open access, we will direct clicks from the abstracts to the publisher website and display the PDF copy on our platform. Clicks to view the full text will be directed to the publisher website, where only users with subscriptions or access through their institution are able to view the full article. . Notably, our quantitative deduction system extends in a natural\nway the equational system for probabilistic bisimilarity given by Stark and\nSmolka by introducing an axiom for dealing with the Kantorovich distance\nbetween probability distributions. The axiomatization is then used to propose a\nmetric extension of a Kleene's style representation theorem for finite labelled\nMarkov chains, that was proposed (in a more general coalgebraic fashion) by\nSilva et al. (Inf. Comput. 2011).\n ","htmlAbstract":null,"createdDate":"2019-10-04T14:13:00.000Z","media":null,"settings":null,"pdfUrl":"https://arxiv.org/pdf/1702.02528","openAccessUrl":null,"authors":{"type":"json","json":["Giorgio Bacci","Giovanni Bacci","Kim G. Larsen","Radu Mardare"]},"contentType":null,"actionButton":null,"journal":{"type":"id","generated":false,"id":"Journal:1156","typename":"Journal"},"headlineImage":null,"__typename":"V4Paper","doi":"arXiv:1702.02528v4","paperUrl":"http://arxiv.org/abs/1702.02528","metrics":{"type":"id","generated":true,"id":"$V4Paper:1625678.metrics","typename":"Metrics"}},"Journal:1156":{"id":"1156","name":"arXiv Computer Science","cover":{"type":"id","generated":true,"id":"$Journal:1156.cover","typename":"Image"},"__typename":"Journal"},"$Journal:1156.cover":{"baseURL":"https://s3-eu-west-1.amazonaws.com/stackademic/assets/journal_cover_arxviv.png","__typename":"Image"},"$V4Paper:1625678.metrics":{"selectedCount":null,"viewedCount":null,"bookmarkedCount":null,"__typename":"Metrics"}}; window.__REDUX_STATE__ = {"feed":{"scrollPos":0,"openAccess":false,"performRefetch":{}},"history":{"historyChanges":0},"onboarding":{"stepsList":[{"stepId":"type","stepName":"What kind of researcher are you?","stepDesc":"","options":[]},{"stepId":"Role","stepName":"What role describes you the best?","stepDesc":"","options":[]},{"stepId":"Org","stepName":"Where do you work or study?","stepDesc":""},{"stepId":"ra","stepName":"Research Areas","stepDesc":"Select the research areas you are interested in","options":[]},{"stepId":"topics","stepName":"Topics","stepDesc":"Select the topics you are interested in","options":[]},{"stepId":"publications","stepName":"Publications","stepDesc":"We have selected some popular publications for you to follow","options":[]},{"stepId":"feeds","stepName":"Feeds","stepDesc":"We have created this feed based on your interests, you can edit and add more from the side menu","options":[]}],"step":1,"loading":false,"loadingText":"Loading...","selections":[{"name":"type","selection":null,"type":"single","mandatory":true},{"name":"role","selection":null,"type":"single","mandatory":true},{"name":"work_study","selection":null,"type":"single","mandatory":false},{"name":"ra","selection":[],"type":"multiple","mandatory":true},{"name":"topics","selection":[],"type":"multiple","mandatory":true},{"name":"publications","selection":[],"type":"multiple","mandatory":false},{"name":"feeds","selection":[],"type":"multiple","mandatory":false}],"topicsNextCursor":null,"topicsFetchingNext":false}}; 3 years ago # A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare 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).

Publisher URL: http://arxiv.org/abs/1702.02528

DOI: arXiv:1702.02528v4

You might also like
Discover & Discuss Important Research

Keeping up-to-date with research can feel impossible, with papers being published faster than you'll ever be able to read them. That's where Researcher comes in: we're simplifying discovery and making important discussions happen. With over 19,000 sources, including peer-reviewed journals, preprints, blogs, universities, podcasts and Live events across 10 research areas, you'll never miss what's important to you. It's like social media, but better. Oh, and we should mention - it's free.

Researcher displays publicly available abstracts and doesn’t host any full article content. If the content is open access, we will direct clicks from the abstracts to the publisher website and display the PDF copy on our platform. Clicks to view the full text will be directed to the publisher website, where only users with subscriptions or access through their institution are able to view the full article.