Document Open Access Logo

Complete Axiomatization for the Bisimilarity Distance on Markov Chains

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.21.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Giorgio Bacci
Giovanni Bacci
Kim G. Larsen
Radu Mardare

Cite AsGet BibTex

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete Axiomatization for the Bisimilarity Distance on Markov Chains. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.21

Abstract

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.
Keywords
  • Markov chains
  • Behavioral distances
  • Axiomatization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational axioms for probabilistic bisimilarity. In AMAST 2002, LNCS, pages 239-253, 2002. Google Scholar
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Bisimulation on Markov Processes over Arbitrary Measurable Spaces. In Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of LNCS, pages 76-95. Springer, 2014. Google Scholar
  3. Jos C. M. Baeten, Jan A. Bergstra, and Scott A. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput., 121(2):234-255, 1995. Google Scholar
  4. Emanuele Bandini and Roberto Segala. Axiomatizations for probabilistic bisimulation. In ICALP, LNCS, pages 370-381, 2001. Google Scholar
  5. Pedro R. D'Argenio, Daniel Gebler, and Matias D. Lee. Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules. In FoSSaCS, LNCS, pages 289-303, 2014. Google Scholar
  6. Yuxin Deng and Catuscia Palamidessi. Axiomatizations for probabilistic finite-state behaviors. Theor. Comput. Sci., 373(1-2):92-114, 2007. Google Scholar
  7. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004. Google Scholar
  8. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov Decision Processes. In Proceedings of the 20th conference on Uncertainty in Artificial Intelligence, UAI, pages 162-169. AUAI Press, 2004. Google Scholar
  9. Daniel Gebler, Kim Guldstrand Larsen, and Simone Tini. Compositional metric reasoning with probabilistic process calculi. In FoSSaCS, LNCS, pages 230-245, 2015. Google Scholar
  10. C. Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. In LICS, pages 186-195. IEEE Computer Society, 1989. Google Scholar
  11. Klaus Keimel and Gordon Plotkin. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science, page ??, 2015. (to appear). Google Scholar
  12. Kim G. Larsen, Uli Fahrenberg, and Claus R. Thrane. Metrics for weighted transition systems: Axiomatization and complexity. Theor. Comput. Sci., 412(28):3358-3369, 2011. Google Scholar
  13. Kim Guldstrand Larsen and Arne Skou. Bisimulation Through Probabilistic Testing. In POPL, pages 344-352, 1989. Google Scholar
  14. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In LICS, page ?? IEEE Computer Society, 2016. (to appear). Google Scholar
  15. Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. Google Scholar
  16. Michael Mislove, Joël Ouaknine, and James Worrell. Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science, 96:7-28, 2004. Google Scholar
  17. Gordon D. Plotkin and John Power. Semantics for algebraic operations. Electr. Notes Theor. Comput. Sci., 45:332-345, 2001. Google Scholar
  18. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Quantitative kleene coalgebras. Inf. Comput., 209(5):822-849, 2011. Google Scholar
  19. Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, MIT Press, pages 571-596, 2000. Google Scholar
  20. Marshall H. Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29(1):25-30, 1949. Google Scholar
  21. Franck van Breugel. On behavioural pseudometrics and closure ordinals. Inf. Process. Lett., 112(19):715-718, 2012. Google Scholar
  22. Franck van Breugel and James Worrell. Towards Quantitative Verification of Probabilistic Transition Systems. In ICALP, volume 2076 of LNCS, pages 421-432, 2001. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact