Document Open Access Logo

The Power of Convex Algebras

Authors Filippo Bonchi, Alexandra Silva, Ana Sokolova

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.23.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Author Details

Filippo Bonchi
Alexandra Silva
Ana Sokolova

Cite As Get BibTex

Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.23

Abstract

Probabilistic automata (PA) combine probability and nondeterminism. 
They can be given different semantics, like strong bisimilarity, 
convex bisimilarity, or (more recently) distribution bisimilarity. 
The latter is based on the view of PA as transformers of probability 
distributions, also called belief states, and promotes distributions 
to first-class citizens.

We give a coalgebraic account of the latter semantics, and explain 
the genesis of the belief-state transformer from a PA. To do so, we 
make explicit the convex algebraic structure present in PA and 
identify belief-state transformers as transition systems with state 
space that carries a convex algebra. As a consequence of our abstract 
approach, we can give a sound proof technique which we call 
bisimulation up-to convex hull.

Subject Classification

Keywords
  • belief-state transformers
  • bisimulation up-to
  • coalgebra
  • convex algebra
  • convex powerset monad
  • probabilistic automata

Metrics

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

References

  1. Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. In Proc LICS'12, pages 55-64. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.17.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Falk Bartels. On generalised coinduction and probabilistic specification formats: distributive laws in coalgebraic modelling. PhD thesis, Vrije Universiteit, Amsterdam, 2004. Google Scholar
  4. Falk Bartels, Ana Sokolova, and Erik de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3-22, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.07.019.
  5. Filippo Bonchi, Daniela Petrişan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In Proc. CSL-LICS'14, pages 20:1-20:9. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603149.
  6. Filippo Bonchi and Damien Pous. Checking nfa equivalence with bisimulations up to congruence. In Proc. POPL'13, pages 457-468. ACM, 2013. URL: http://dx.doi.org/10.1145/2429069.2429124.
  7. Ivica Bošnjak and Rozálija Madarász. On power structures. Algebra and Discrete Mathematics, 2:14-35, 2003. Google Scholar
  8. Ivica Bošnjak and Rozálija Madarász. Some results on complex algebras of subalgebras. Novi Sad Journal of Mathematics, 237(2):231-240, 2007. Google Scholar
  9. C. Brink. On power structures. Algebra Universalis, 30:177-216, 1993. Google Scholar
  10. Pablo Samuel Castro, Prakash Panangaden, and Doina Precup. Equivalence relations in fully and partially observable Markov decision processes. In Proc. IJCAI'09, pages 1653-1658, 2009. URL: http://ijcai.org/Proceedings/09/Papers/276.pdf.
  11. Silvia Crafa and Francesco Ranzato. A spectrum of behavioral relations over LTSs on probability distributions. In Proc. CONCUR'11, pages 124-139. LNCS 6901, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_9.
  12. Fredrik Dahlqvist, Vincent Danos, and Ilias Garnier. Robustly parameterised higher-order probabilistic models. In Proc. CONCUR'16, pages 23:1-23:15. LIPIcs 50, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.23.
  13. Yuxin Deng and Matthew Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013. URL: http://dx.doi.org/10.1016/j.ic.2012.10.010.
  14. Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science, 4(4), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(4:4)2008.
  15. Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes. In Proc. CONCUR'09, pages 274-288. LNCS 5710, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04081-8_19.
  16. Ernst-Erich Doberkat. Eilenberg-Moore algebras for stochastic relations. Information and Computation, 204(12):1756-1781, 2006. URL: http://dx.doi.org/10.1016/j.ic.2006.09.001.
  17. Ernst-Erich Doberkat. Erratum and addendum: Eilenberg-Moore algebras for stochastic relations [mr2277336]. Information and Computation, 206(12):1476-1484, 2008. URL: http://dx.doi.org/10.1016/j.ic.2008.08.002.
  18. Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science, 19(3):549-563, 2008. URL: http://dx.doi.org/10.1142/S0129054108005814.
  19. Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Limit synchronization in Markov decision processes. In Proc. FOSSACS'14, pages 58-72. LNCS 8412, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_4.
  20. Christian Eisentraut, Holger Hermanns, Julia Krämer, Andrea Turrini, and Lijun Zhang. Deciding bisimilarities on distributions. In Proc. QEST'13, pages 72-88. LNCS 8054, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40196-1_6.
  21. Christian Eisentraut, Holger Hermanns, and Lijun Zhang. On probabilistic automata in continuous time. In Proc. LICS'10, pages 342-351. IEEE, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.41.
  22. Yuan Feng and Lijun Zhang. When equivalence and bisimulation join forces in probabilistic automata. In Proc. FM'14, pages 247-262. LNCS 8442, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06410-9_18.
  23. Tobias Fritz. Convex spaces I: Definition and Examples, 2015. arXiv:0903.5522v3 [math.MG]. Google Scholar
  24. Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. Church: a language for generative models. CoRR, abs/1206.3255, 2012. URL: http://arxiv.org/abs/1206.3255.
  25. Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012. URL: http://dx.doi.org/10.1007/s00165-012-0242-7.
  26. Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In Proc. CONCUR'14, pages 249-265. LNCS 8704, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_18.
  27. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. CoRR, abs/1701.02547, 2017. URL: http://arxiv.org/abs/1701.02547.
  28. Bart Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electronic Notes in Theoretical Computer Science, 203(5):131-152, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.05.023.
  29. Bart Jacobs. Convexity, duality and effects. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 1-19. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15240-5_1.
  30. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: http://dx.doi.org/10.1017/CBO9781316823187.
  31. Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS, 62:222-259, 1997. Google Scholar
  32. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. Journal of Computer and System Sciences, 81(5):859-879, 2015. URL: http://dx.doi.org/10.1016/j.jcss.2014.12.005.
  33. Bart Jacobs, Bas Westerbaan, and Bram Westerbaan. States of convex sets. In Proc. FOSSACS'15, pages 87-101. LNCS 9034, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_6.
  34. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.03.023.
  35. Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about mdps as transformers of probability distributions. In Proc. QEST'10, pages 199-208. IEEE, 2010. URL: http://dx.doi.org/10.1109/QEST.2010.35.
  36. Alexander Kurz. Logics for Coalgebras and Applications to Computer Science. PhD thesis, Ludwig-Maximilians-Universität München, 2000. Google Scholar
  37. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. CAV'11, pages 585-591. LNCS 6806, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22110-1_47.
  38. Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1):101-150, 2002. URL: http://dx.doi.org/10.1016/S0304-3975(01)00046-9.
  39. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1-28, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90030-6.
  40. Axel Legay, Andrzej S. Murawski, Joël Ouaknine, and James Worrell. On automated verification of probabilistic programs. In Proc. TACAS'08, pages 173-187. LNCS 4963, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_13.
  41. Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D. Nielsen, Kim G. Larsen, and Brian Nielsen. Learning deterministic probabilistic automata from a model checking perspective. Machine Learning, 105(2):255-299, 2016. URL: http://dx.doi.org/10.1007/s10994-016-5565-9.
  42. Robin Milner. Communication and concurrency, volume 84 of PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  43. Matteo Mio. Upper-expectation bisimilarity and łukasiewicz μ-calculus. In Proc. FOSSACS'14, pages 335-350. LNCS 8412, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_22.
  44. Michael W. Mislove. Discrete random variables over domains, revisited. In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pages 185-202. LNCS 10160, 2017. URL: http://dx.doi.org/10.1007/978-3-319-51046-0_10.
  45. Damien Pous and Davide Sangiorgi. Enhancements of the coinductive proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  46. Jan Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3-80, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00056-6.
  47. Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages. In Proc. POPL'16, pages 595-607. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837651.
  48. Rolf Schneider. Convex bodies: the Brunn-Minkowski theory, volume 44 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993. URL: http://dx.doi.org/10.1017/CBO9780511526282.
  49. Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995. Google Scholar
  50. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. In Proc. CONCUR'94, pages 481-496. LNCS 836, 1994. URL: http://dx.doi.org/10.1007/978-3-540-48654-1_35.
  51. Zbigniew Semadeni. Monads and their Eilenberg-Moore algebras in functional analysis. Queen’s University, Kingston, Ont., 1973. Queen’s Papers in Pure and Applied Mathematics, No. 33. Google Scholar
  52. Falak Sher and Joost-Pieter Katoen. Compositional abstraction techniques for probabilistic automata. In Proc. TCS'12, pages 325-341. LNCS 7604, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33475-7_23.
  53. Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing the powerset construction, coalgebraically. In Proc. FSTTCS'10, pages 272-283. LIPIcs 8, 2010. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.272.
  54. Ana Sokolova. Probabilistic systems coalgebraically: A survey. Theoretical Computer Science, 412(38):5095-5110, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.05.008.
  55. Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110-3148, 2015. URL: http://dx.doi.org/10.1016/j.jpaa.2014.10.005.
  56. Ana Sokolova and Harald Woracek. Termination in convex sets of distributions. In Proc. CALCO '17. LIPIcs, 2017. To appear. Google Scholar
  57. Sam Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science, 7(1), 2011. URL: http://dx.doi.org/10.2168/LMCS-7(1:13)2011.
  58. Sam Staton. Commutative semantics for probabilistic programming. In Proc. ESOP'17, pages 855-879. LNCS 10201, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_32.
  59. Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. LICS'16, pages 525-534. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2935313.
  60. M.H. Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata. Serie Quarta, 29:25-30, 1949. URL: http://dx.doi.org/10.1007/BF02413910.
  61. T. Świrszcz. Monadic functors and convexity. Bulletin de l'Académie Polonaise des Sciences. Série des Sciences Mathématiques, Astronomiques et Physiques, 22:39-42, 1974. Google Scholar
  62. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. LICS'97, pages 280-291. IEEE, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614955.
  63. Daniele Varacca. Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. PhD thesis, Univ. Aarhus, 2003. BRICS Dissertation Series, DS-03-14. Google Scholar
  64. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87-113, 2006. URL: http://dx.doi.org/10.1017/S0960129505005074.
  65. Erik de Vink and Jan Rutten. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science, 221:271-293, 1999. URL: http://dx.doi.org/10.1016/S0304-3975(99)00035-3.
  66. Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. High-level counterexamples for probabilistic automata. Logical Methods in Computer Science, 11(1), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:15)2015.
  67. Uwe Wolter. On corelations, cokernels, and coequations. Electronic Notes in Theoretical Computer Science, 33, 2000. URL: http://dx.doi.org/10.1016/S1571-0661(05)80355-X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact