Document Open Access Logo

Domain Reasoning in TopKAT

Authors Cheng Zhang , Arthur Azevedo de Amorim , Marco Gaboardi

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.157.pdf
  • Filesize: 0.69 MB
  • 18 pages

Document Identifiers

Author Details

Cheng Zhang
  • Boston University, MA, USA
Arthur Azevedo de Amorim
  • Rochester Institute of Technology, NY, USA
Marco Gaboardi
  • Boston University, MA, USA

Funding

  • Zhang, Cheng: National Science Foundation Grant No. 2040249 and No. 2314324
  • de Amorim, Arthur Azevedo: National Science Foundation Grant No. 2314323
  • Gaboardi, Marco: National Science Foundation Grant No. 2040249 and No. 2314324

Cite AsGet BibTex

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.157

Abstract

TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Programming logic
Keywords
  • Kleene algebra
  • Kleene Algebra With Tests
  • Kleene Algebra With Domain
  • Kleene Algebra With Top and Tests
  • Completeness
  • Decidability

Metrics

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

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks. ACM SIGPLAN Notices, 49(1):113-126, January 2014. URL: https://doi.org/10.1145/2578855.2535862.
  2. Hajnal Andréka and Szabolcs Mikulás. Axiomatizability of positive algebras of binary relations. Algebra universalis, 66(1-2):7-34, October 2011. URL: https://doi.org/10.1007/s00012-011-0142-3.
  3. Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. An Algebra of Alignment for Relational Verification. Proceedings of the ACM on Programming Languages, 7(POPL):20:573-20:603, January 2023. URL: https://doi.org/10.1145/3571213.
  4. Stanley Burris and H. P. Sankappanavar. A Course in Universal Algebra. Number 78 in Graduate Texts in Mathematics. Springer-Verlag, New York, 1981. Google Scholar
  5. Ernie Cohen. Hypotheses in kleene algebra, March 1995. Google Scholar
  6. Ernie Cohen, Dexter Kozen, and Frederick Smith. The Complexity of Kleene Algebra with Tests. Technical Report, Cornell University, USA, June 1996. Google Scholar
  7. Edsko de Vries and Vasileios Koutavas. Reverse Hoare Logic. In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, Software Engineering and Formal Methods, volume 7041, pages 155-171. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-24690-6_12.
  8. Jules Desharnais, Bernhard Möller, and Georg Struth. Modal kleene algebra and applications – a survey. In Journal on Relational Methods in Computer Science, pages 93-131, 2004. Google Scholar
  9. Jules Desharnais, Bernhard Möller, and Georg Struth. Kleene algebra with domain. ACM Transactions on Computational Logic, 7(4):798-833, October 2006. URL: https://doi.org/10.1145/1183278.1183285.
  10. Jules Desharnais and Georg Struth. Internal axioms for domain semirings. Science of Computer Programming, 76(3):181-203, March 2011. URL: https://doi.org/10.1016/j.scico.2010.05.007.
  11. Amina Doumane, Denis Kuperberg, Damien Pous, and Pierre Pradic. Kleene algebra with hypotheses. In 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Proc. FoSSaCS 2019, Prague, Czech Republic, 2019. Springer. Google Scholar
  12. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiánski. Domain semirings united. arXiv:2011.04704 [cs], March 2021. Google Scholar
  13. Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. Kat + b! In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, pages 1-10, New York, NY, USA, July 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603095.
  14. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, and Huibiao Zhu. Developments in concurrent kleene algebra. Journal of Logical and Algebraic Methods in Programming, 85(4):617-636, June 2016. URL: https://doi.org/10.1016/j.jlamp.2015.09.012.
  15. Peter Höfner and Georg Struth. Automated Reasoning in Kleene Algebra. In Frank Pfenning, editor, Automated Deduction endash CADE-21, Lecture Notes in Computer Science, pages 279-294, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-73595-3_19.
  16. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness, volume 12077 of Lecture Notes in Computer Science, pages 381-400. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  17. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent kleene algebra: Free model and completeness. In Amal Ahmed, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 856-882, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_30.
  18. D. Kozen. A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, May 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  19. Dexter Kozen. Kleene algebra with tests and commutativity conditions, volume 1055 of Lecture Notes in Computer Science, pages 14-33. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61042-1_35.
  20. Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL: https://doi.org/10.1145/256167.256195.
  21. Dexter Kozen. On hoare logic and kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60-76, July 2000. URL: https://doi.org/10.1145/343369.343378.
  22. Dexter Kozen. On the complexity of reasoning in kleene algebra. Information and Computation, 179(2):152-162, December 2002. URL: https://doi.org/10.1006/inco.2001.2960.
  23. Dexter Kozen and Alexandra Silva. Left-handed completeness. Theoretical Computer Science, 807:220-233, February 2020. URL: https://doi.org/10.1016/j.tcs.2019.10.040.
  24. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability, volume 1258 of Lecture Notes in Computer Science, pages 244-259. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. URL: https://doi.org/10.1007/3-540-63172-0_43.
  25. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. Finding real bugs in big programs with incorrectness logic. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1-27, April 2022. URL: https://doi.org/10.1145/3527325.
  26. Konstantinos Mamouras. Equational Theories of Abnormal Termination Based on Kleene Algebra, volume 10203 of Lecture Notes in Computer Science, pages 88-105. Springer Berlin Heidelberg, Berlin, Heidelberg, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_6.
  27. Ernest G. Manes and Michael A. Arbib. Algebraic Approaches to Program Semantics. Springer New York, New York, NY, 1986. Google Scholar
  28. Brett McLean. Free Kleene algebras with domain. Journal of Logical and Algebraic Methods in Programming, 117:100606, December 2020. URL: https://doi.org/10.1016/j.jlamp.2020.100606.
  29. Toby Murray. An Under-Approximate Relational Logic. Archive of Formal Proofs, March 2020. Google Scholar
  30. Bernhard Möller, Peter O’Hearn, and Tony Hoare. On Algebra of Program Correctness and Incorrectness, volume 13027 of Lecture Notes in Computer Science, pages 325-343. Springer International Publishing, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-88701-8_20.
  31. Peter W. O’Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-32, January 2020. URL: https://doi.org/10.1145/3371078.
  32. Damien Pous. On the Positive Calculus of Relations with Transitive Closure. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.3.
  33. Damien Pous, Jurriaan Rot, and Jana Wagemaker. On tools for completeness of kleene algebra with hypotheses. In Relational and Algebraic Methods in Computer Science: 19th International Conference, RAMiCS 2021, Marseille, France, November 2–5, 2021, Proceedings, pages 378-395, Berlin, Heidelberg, November 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-88701-8_23.
  34. Damien Pous and Jana Wagemaker. Completeness theorems for kleene algebra with top. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR 2022), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.26.
  35. Damien Pous and Jana Wagemaker. Completeness theorems for kleene algebra with tests and top. CoRR, April 2023. URL: https://arxiv.org/abs/2304.07190.
  36. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic, volume 12225 of Lecture Notes in Computer Science, pages 225-252. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_14.
  37. Igor Sedlár. On the complexity of kleene algebra with domain. In Relational and Algebraic Methods in Computer Science: 20th International Conference, RAMiCS 2023, Augsburg, Germany, April 3–6, 2023, Proceedings, pages 208-223, Berlin, Heidelberg, April 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-28083-2_13.
  38. 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. Proceedings of the ACM on Programming Languages, 4(POPL):1-28, January 2020. URL: https://doi.org/10.1145/3371129.
  39. Georg Struth. On the expressive power of kleene algebra with domain. CoRR, August 2015. URL: https://arxiv.org/abs/1507.07246.
  40. Alfred Tarski. On the calculus of relations. Journal of Symbolic Logic, 6(3):73-89, September 1941. URL: https://doi.org/10.2307/2268577.
  41. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and kleene algebra with top and tests. CoRR, August 2022. URL: https://doi.org/10.48550/arXiv.2108.07707.
  42. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and kleene algebra with top and tests. Proceedings of the ACM on Programming Languages, 6(POPL):29:1-29:30, January 2022. URL: https://doi.org/10.1145/3498690.
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