Document Open Access Logo

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Authors Wojciech Różowski , Tobias Kappé , Dexter Kozen , Todd Schmid , Alexandra Silva

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.136.pdf
  • Filesize: 0.94 MB
  • 20 pages

Document Identifiers

Author Details

Wojciech Różowski
  • Department of Computer Science, University College London, UK
Tobias Kappé
  • Open Universiteit, Heerlen, The Netherlands
  • ILLC, University of Amsterdam, The Netherlands
Dexter Kozen
  • Department of Computer Science, Cornell University, Ithaca, NY, USA
Todd Schmid
  • Department of Computer Science, University College London, UK
Alexandra Silva
  • Department of Computer Science, Cornell University, Ithaca, NY, USA

Funding

This work was partially supported by ERC grant Autoprobe (no. 101002697; Różowski, Schmid and Silva), the EU’s Horizon 2020 research and innovation program under Marie Skłodowska-Curie grant VERLAN (no. 101027412; Kappé), and NSF grant CCF-2008083 (Kozen).

Cite AsGet BibTex

Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 136:1-136:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.136

Abstract

We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n³ log n) time via a generic partition refinement algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
Keywords
  • Kleene Algebra with Tests
  • program equivalence
  • completeness
  • coalgebra

Metrics

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

Related Versions

References

  1. Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational axioms for probabilistic bisimilarity. In AMAST, pages 239-253, 2002. URL: https://doi.org/10.1007/3-540-45719-4_17.
  2. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: semantic foundations for networks. In POPL, pages 113-126, 2014. URL: https://doi.org/10.1145/2535838.2535862.
  3. Allegra Angus and Dexter Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Cornell University, July 2001. URL: https://hdl.handle.net/1813/5831.
  4. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete axiomatization for the bisimilarity distance on Markov chains. In CONCUR, pages 21:1-21:14, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.21.
  5. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  6. Emanuele Bandini and Roberto Segala. Axiomatizations for probabilistic bisimulation. In ICALP, pages 370-381, 2001. URL: https://doi.org/10.1007/3-540-48224-5_31.
  7. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  8. Falk Bartels, Ana Sokolova, and Erik P. de Vink. A hierarchy of probabilistic system types. In CMCS, pages 57-75, 2003. URL: https://doi.org/10.1016/S1571-0661(04)80632-7.
  9. Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors. Foundations of Probabilistic Programming. Cambridge University Press, Cambridge, 2020. URL: https://doi.org/10.1017/9781108770750.
  10. Jan A. Bergstra and Jan Willem Klop. Verification of an alternating bit protocol by means of process algebra. In Mathematical Methods of Specification and Synthesis of Software Systems, volume 215 of LNCS, pages 9-23. Springer, 1985. URL: https://doi.org/10.1007/3-540-16444-8_1.
  11. Jan A. Bergstra and Jan Willem Klop. Process theory based on bisimulation semantics. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 50-122, 1988. URL: https://doi.org/10.1007/BFb0013021.
  12. Stephen L. Bloom and Zoltán Ésik. Iteration Theories - The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer, 1993. URL: https://doi.org/10.1007/978-3-642-78034-9.
  13. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  14. Ernie Cohen. Hypotheses in Kleene algebra. Technical report, Bellcore, 1994. Google Scholar
  15. Ernie Cohen. Lazy caching in Kleene algebra. Technical report, Bellcore, 1994. Google Scholar
  16. Erik P. de Vink and Jan J. M. M. Rutten. Bisimulation for probabilistic transition systems: A coalgebraic approach. Theor. Comput. Sci., 221(1-2):271-293, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00035-3.
  17. Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic partition refinement and weighted tree automata. In FM, pages 280-297, 2019. URL: https://doi.org/10.1007/978-3-030-30942-8_18.
  18. Josée Desharnais. Labelled Markov processes. PhD thesis, McGill University, 1999. Google Scholar
  19. Amina Doumane, Denis Kuperberg, Damien Pous, and Pierre Pradic. Kleene algebra with hypotheses. In FoSSaCS, pages 207-223, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_12.
  20. Calvin C. Elgot. Monadic computation and iterative algebraic theories. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175-230. Elsevier, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71949-9.
  21. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In ESOP, pages 282-309, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_12.
  22. Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In POPL, pages 343-355, 2015. URL: https://doi.org/10.1145/2676726.2677011.
  23. Leandro Gomes, Alexandre Madeira, and Luís Soares Barbosa. Generalising KAT to verify weighted computations. Sci. Ann. Comput. Sci., 29(2):141-184, 2019. URL: https://doi.org/10.7561/SACS.2019.2.141.
  24. Alexandre Goy and Daniela Petrisan. Combining probabilistic and non-deterministic choice via weak distributive laws. In LICS, pages 454-464, 2020. URL: https://doi.org/10.1145/3373718.3394795.
  25. Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. KAT + B! In CSL, pages 44:1-44:10, 2014. URL: https://doi.org/10.1145/2603088.2603095.
  26. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In ICALP, pages 299-309, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  27. Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pages 375-404, 2006. URL: https://doi.org/10.1007/11780274_20.
  28. Bart Jacobs. From multisets over distributions to distributions over multisets. In LICS, pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470678.
  29. Jules Jacobs and Thorsten Wißmann. Fast coalgebraic bisimilarity minimization. In POPL, pages 1514-1541, 2023. URL: https://doi.org/10.1145/3571245.
  30. Claire Jones. Probabilistic non-determinism. PhD thesis, University of Edinburgh, UK, 1990. URL: https://hdl.handle.net/1842/413.
  31. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. In PODC, pages 228-240, 1983. URL: https://doi.org/10.1145/800221.806724.
  32. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43-68, 1990. URL: https://doi.org/10.1016/0890-5401(90)90025-D.
  33. Tobias Kappé, Todd Schmid, and Alexandra Silva. A complete inference system for skip-free guarded Kleene algebra with tests. In ESOP, pages 309-336, 2023. URL: https://doi.org/10.1007/978-3-031-30044-8_12.
  34. Donald E. Knuth and Andrew C. Yao. The complexity of nonuniform random number generation. In Algorithms and Complexity: New Directions and Recent Results, 1976. Google Scholar
  35. Dexter Kozen. On the complexity of reasoning in Kleene algebra. Inf. Comput., 179(2):152-162, 2002. URL: https://doi.org/10.1006/inco.2001.2960.
  36. Dexter Kozen and Konstantinos Mamouras. Kleene algebra with equations. In ICALP (Part II), pages 280-292, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_24.
  37. Dexter Kozen and Maria-Christina Patron. Certification of compiler optimizations using Kleene algebra with tests. In CL, pages 568-582, 2000. URL: https://doi.org/10.1007/3-540-44957-4_38.
  38. Dexter Kozen and Alexandra Silva. Multisets and distributions, 2023. URL: https://arxiv.org/abs/2301.10812.
  39. Dexter Kozen and Wei-Lung Dustin Tseng. The Böhm-Jacopini theorem is false, propositionally. In MPC, pages 177-192, 2008. URL: https://doi.org/10.1007/978-3-540-70594-9_11.
  40. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  41. Hosam Mahmoud. Pólya Urn Models. Texts in Statistical Science. Chapman & Hall, 2008. Google Scholar
  42. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In LICS, pages 700-709, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  43. Annabelle McIver, Carlos Gonzalía, Ernie Cohen, and Carroll C. Morgan. Using probabilistic Kleene algebra pKA for protocol verification. J. Log. Algebraic Methods Program., 76(1):90-111, 2008. URL: https://doi.org/10.1016/j.jlap.2007.10.005.
  44. Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. On probabilistic Kleene algebras, automata and simulations. In RAMICS, pages 264-279, 2011. URL: https://doi.org/10.1007/978-3-642-21070-9_20.
  45. Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. Probabilistic concurrent Kleene algebra. In QAPL, pages 97-115, 2013. URL: https://doi.org/10.4204/EPTCS.117.7.
  46. Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. URL: https://doi.org/10.1016/0022-0000(84)90023-0.
  47. Michael W. Mislove, Joël Ouaknine, and James Worrell. Axioms for probability and nondeterminism. In EXPRESS, pages 7-28, 2003. URL: https://doi.org/10.1016/j.entcs.2004.04.019.
  48. Robert Paige and Robert Endre Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973-989, 1987. URL: https://doi.org/10.1137/0216062.
  49. Damien Pous, Jurriaan Rot, and Jana Wagemaker. On tools for completeness of kleene algebra with hypotheses, 2022. URL: https://arxiv.org/abs/2210.13020.
  50. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  51. Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity, 2023. URL: https://arxiv.org/abs/2305.01755.
  52. Arto Salomaa. Two complete axiom systems for the algebra of regular events. J. ACM, 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.
  53. Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. In ICALP, pages 142:1-142:14, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.142.
  54. Todd Schmid, Jurriaan Rot, and Alexandra Silva. On star expressions and coalgebraic completeness theorems. In MFPS, pages 242-259, 2021. URL: https://doi.org/10.4204/EPTCS.351.15.
  55. Todd Schmid, Wojciech Różowski, Alexandra Silva, and Jurriaan Rot. Processes parametrised by an algebraic theory. In ICALP, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.132.
  56. Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. In CONCUR, pages 481-496, 1994. URL: https://doi.org/10.1007/978-3-540-48654-1_35.
  57. Alexandra Silva. Kleene coalgebra. PhD thesis, University of Nijmegen, 2010. Google Scholar
  58. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In POPL, pages 61:1-61:28, 2020. URL: https://doi.org/10.1145/3371129.
  59. Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: semantic foundations for probabilistic networks. In POPL, pages 557-571, 2017. URL: https://doi.org/10.1145/3009837.3009843.
  60. Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. Scalable verification of probabilistic networks. In PLDI, pages 190-203, 2019. URL: https://doi.org/10.1145/3314221.3314639.
  61. Ana Sokolova. Probabilistic systems coalgebraically: A survey. Theor. Comput. Sci., 412(38):5095-5110, 2011. URL: https://doi.org/10.1016/j.tcs.2011.05.008.
  62. 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, pages 571-596, 2000. Google Scholar
  63. Sam Staton. Relating coalgebraic notions of bisimulation. Log. Methods Comput. Sci., 7(1), 2011. URL: https://doi.org/10.2168/LMCS-7(1:13)2011.
  64. Joseph Aaron Toumanios. Three sided die, 2019. US patent 10384119. URL: https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/10384119.
  65. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87-113, 2006. URL: https://doi.org/10.1017/S0960129505005074.
  66. Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, and Alexandra Silva. Concurrent NetKAT - Modeling and analyzing stateful, concurrent networks. In ESOP, pages 575-602, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_21.
  67. Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and modular coalgebraic partition refinement. Logical Methods in Computer Science, 16:1:8:1-8:63, 2020. URL: https://doi.org/10.23638/LMCS-16(1:8)2020.
  68. Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Quasilinear-time computation of generic modal witnesses for behavioural inequivalence. Log. Methods Comput. Sci., 18(4), 2022. URL: https://doi.org/10.46298/lmcs-18(4:6)2022.
  69. James Worrell. On the final sequence of a finitary set functor. Theor. Comput. Sci., 338(1-3):184-199, 2005. URL: https://doi.org/10.1016/j.tcs.2004.12.009.
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 Imprint Privacy Contact