Document Open Access Logo

Weighted GKAT: Completeness and Complexity

Authors Spencer Van Koevering , Wojciech Różowski , Alexandra Silva

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.172.pdf
  • Filesize: 0.95 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Weighted Programming
  • Automata
  • Axiomatization
  • Decision Procedure

Metrics

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

Abstract

We propose Weighted Guarded Kleene Algebra with Tests (wGKAT), an uninterpreted weighted programming language equipped with branching, conditionals, and loops. We provide an operational semantics for wGKAT using a variant of weighted automata and introduce a sound and complete axiomatization. We also provide a polynomial time decision procedure for bisimulation equivalence.

Cite As Get BibTex

Spencer Van Koevering, Wojciech Różowski, and Alexandra Silva. Weighted GKAT: Completeness and Complexity. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 172:1-172:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.172

Author Details

Spencer Van Koevering
  • Cornell University, Ithaca, NY, USA
Wojciech Różowski
  • University College London, UK
Alexandra Silva
  • Cornell University, Ithaca, NY, USA

Funding

  • Van Koevering, Spencer: Partially supported by a Cornell Bowers CIS Deans Excellence Fellowship.
  • Różowski, Wojciech: Partially supported by ERC grant Autoprobe (grant agreement 101002697).
  • Silva, Alexandra: Partially supported by ONR grant N68335-22-C-0411, ERC grant 101002697, and a Royal Society Wolfson fellowship.

References

  1. Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. Weighted Programming, 2022. URL: https://doi.org/10.48550/arXiv.2202.07577.
  2. Jan A. Bergstra and Jan Willem Klop. Verification of an alternating bit protocol by means of process algebra. In Wolfgang Bibel and Klaus P. Jantke, editors, Mathematical Methods of Specification and Synthesis of Software Systems '85, Proceedings of the International Spring School, Wendisch-Rietz, GDR, April 22-26, 1985, volume 215 of Lecture Notes in Computer Science, pages 9-23, Berlin, Heidelberg, 1985. Springer. URL: https://doi.org/10.1007/3-540-16444-8_1.
  3. Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic Partition Refinement and Weighted Tree Automata. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods - The Next 30 Years, pages 280-297, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30942-8_18.
  4. Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement, 2017. URL: https://doi.org/10.48550/arXiv.1705.08362.
  5. M Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer-Verlag, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5.
  6. Zoltán Ésik. Iteration Semirings. In Masami Ito and Masafumi Toyama, editors, Developments in Language Theory, pages 1-20, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-85780-8_1.
  7. Zoltán Ésik and Werner Kuich. Inductive star-semirings. Theor. Comput. Sci., 324(1):3-33, 2004. Words, Languages and Combinatorics. URL: https://doi.org/10.1016/j.tcs.2004.03.050.
  8. Jonathan S Golan. Semirings and their Applications. Springer Science & Business Media, 2013. URL: https://doi.org/10.1007/978-94-015-9333-5.
  9. H Peter Gumm. Copower functors. Theoretical Computer Science, 410(12-13):1129-1142, 2009. URL: https://doi.org/10.1016/j.tcs.2008.09.057.
  10. H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science, 44(1):185-204, 2001. CMCS 2001, Coalgebraic Methods in Computer Science (a Satellite Event of ETAPS 2001). URL: https://doi.org/10.1016/S1571-0661(04)80908-3.
  11. H. Peter Gumm and Tobias Schröder. Coalgebras Of Bounded Type. Math. Struct. Comput. Sci., 12(5):565-578, 2002. URL: https://doi.org/10.1017/S0960129501003590.
  12. Paris C. Kanellakis and Scott A. Smolka. CCS Expressions, Finite State Processes, and THree Problems of Equivalence. In Robert L. Probert, Nancy A. Lynch, and Nicola Santoro, editors, Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 17-19, 1983, PODC '83, pages 228-240, New York, NY, USA, 1983. ACM. URL: https://doi.org/10.1145/800221.806724.
  13. Spencer Van Koevering, Wojciech Różowski, and Alexandra Silva. Weighted GKAT: Completeness and Complexity, 2025. URL: https://arxiv.org/abs/2504.20385.
  14. Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  15. Dexter Kozen. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, May 1997. URL: https://doi.org/10.1145/256167.256195.
  16. Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In W. Kuich, editor, Automata, Languages and Programming, pages 101-112, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-55719-9_67.
  17. Robert Paige and Robert E. Tarjan. Three Partition Refinement Algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. URL: https://doi.org/10.1137/0216062.
  18. H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. Electronic Notes in Theoretical Computer Science, 33:111-131, 2000. CMCS'2000, Coalgebraic Methods in Computer Science. URL: https://doi.org/10.1016/S1571-0661(05)80346-9.
  19. 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.
  20. Jan J. M. M. Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theor. Comput. Sci., 308(1-3):1-53, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00895-2.
  21. Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity, 2023. URL: https://doi.org/10.48550/arXiv.2305.01755.
  22. Arto Salomaa. Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM, 13(1):158-169, January 1966. URL: https://doi.org/10.1145/321312.321326.
  23. Todd Junior Wayne Schmid. Coalgebraic Completeness Theorems for Effectful Process Algebras. PhD thesis, UCL (University College London), 2024. Google Scholar
  24. Igor Sedlár. Kleene Algebra With Tests for Weighted Programs. 2023 IEEE 53rd International Symposium on Multiple-Valued Logic (ISMVL), pages 111-116, 2023. URL: https://doi.org/10.48550/arXiv.2303.00322.
  25. 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, December 2019. URL: https://doi.org/10.1145/3371129.
  26. Friedrich Wehrung. Refinement Monoids, Equidecomposability Types, and Boolean Inverse Semigroups, volume 2188 of Lecture Notes in Mathematics. Springer International Publishing, Cham, 1st edition 2017 edition, 2017. URL: https://doi.org/10.1007/978-3-319-61599-8.
  27. Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science, 16, 2020. URL: https://doi.org/10.23638/LMCS-16(1:8)2020.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact