Document Open Access Logo

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Authors Todd Schmid , Tobias Kappé , Dexter Kozen , Alexandra Silva

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.142.pdf
  • Filesize: 0.9 MB
  • 14 pages

Document Identifiers

Author Details

Todd Schmid
  • Department of Computer Science, University College London, UK
Tobias Kappé
  • Department of Computer Science, Cornell University, Ithaca, NY, USA
Dexter Kozen
  • Department of Computer Science, Cornell University, Ithaca, NY, USA
Alexandra Silva
  • Department of Computer Science, University College London, UK

Funding

  • Kappé, Tobias: DARPA grant HR001120C0107 (Pronto)
  • Kozen, Dexter: NSF grant CCF-2008083
  • Silva, Alexandra: ERC Consolidator Grant AutoProbe (101002697) and a Royal Society Wolfson Fellowship

Cite AsGet BibTex

Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 142:1-142:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.142

Abstract

Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to these behaviors. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
Keywords
  • Kleene algebra
  • program equivalence
  • completeness
  • coequations

Metrics

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

Related Versions

References

  1. Jirí Adámek. A logic of coequations. In CSL, pages 70-86, 2005. URL: https://doi.org/10.1007/11538363_7.
  2. Jirí Adámek, Stefan Milius, Robert S. R. Myers, and Henning Urbat. Generalized Eilenberg theorem: Varieties of languages in a category. ACM Trans. Comput. Log., 20(1):3:1-3:47, 2019. URL: https://doi.org/10.1145/3276771.
  3. Jirí Adámek and Hans-E. Porst. On varieties and covarieties in a category. Math. Struct. Comput. Sci., 13(2):201-232, 2003. URL: https://doi.org/10.1017/S0960129502003882.
  4. 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.
  5. Adolfo Ballester-Bolinches, Enric Cosme-Llópez, and Jan J. M. M. Rutten. The dual equivalence of equations and coequations for automata. Inf. Comput., 244:49-75, 2015. URL: https://doi.org/10.1016/j.ic.2015.08.001.
  6. Corrado Böhm and Giuseppe Jacopini. Flow diagrams, Turing machines and languages with only two formation rules. Commun. ACM, 9(5):366-371, 1966. URL: https://doi.org/10.1145/355592.365646.
  7. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  8. Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report TR96-1598, Cornell University, July 1996. URL: https://hdl.handle.net/1813/7253.
  9. 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.
  10. Nate Foster, Dexter Kozen, Matthew 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.
  11. Clemens Grabmayer and Wan J. Fokkink. A complete proof system for 1-free regular expressions modulo bisimilarity. In LICS, pages 465-478, 2020. URL: https://doi.org/10.1145/3373718.3394744.
  12. H. Gumm. Elements of the general theory of coalgebras, 2000. Google Scholar
  13. David Harel. On folk theorems. Commun. ACM, 23(7):379-389, 1980. URL: https://doi.org/10.1145/358886.358892.
  14. 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.
  15. Donald M. Kaplan. Regular expressions and the equivalence of programs. J. Comput. Syst. Sci., 3(4):361-386, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80027-9.
  16. Stephen C. Kleene. Representation of events in nerve nets and finite automata. In Claude E. Shannon and John McCarthy, editors, Automata Studies, pages 3-41. Princeton University Press, 1956. Google Scholar
  17. Dexter Kozen. Kleene algebra with tests and commutativity conditions. In TACAS, pages 14-33, 1996. URL: https://doi.org/10.1007/3-540-61042-1_35.
  18. Dexter Kozen. Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In STACS, pages 27-38, 2001. URL: https://doi.org/10.1007/3-540-44693-1_3.
  19. Dexter Kozen. Automata on guarded strings and applications. Matematica Contemporanea, 24:117-139, 2003. Google Scholar
  20. Dexter Kozen. Nonlocal flow of control and Kleene algebra with tests. In LICS, pages 105-117, 2008. URL: https://doi.org/10.1109/LICS.2008.32.
  21. Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. In Can Başkent, Lawrence S. Moss, and Ramaswamy Ramanujam, editors, Rohit Parikh on Logic, Language and Society, volume 11 of Outstanding Contributions to Logic, pages 279-298. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-47843-2_15.
  22. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In CSL, pages 244-259, 1996. URL: https://doi.org/10.1007/3-540-63172-0_43.
  23. 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.
  24. Konstantinos Mamouras. Equational theories of abnormal termination based on Kleene algebra. In FOSSACS, volume 10203 of Lecture Notes in Computer Science, pages 88-105, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_6.
  25. 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.
  26. Dusko Pavlovic and Martín Hötzel Escardó. Calculus in coinductive form. In LICS, pages 408-417, 1998. URL: https://doi.org/10.1109/LICS.1998.705675.
  27. 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.
  28. 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.
  29. Julian Salamanca, Adolfo Ballester-Bolinches, Marcello M. Bonsangue, Enric Cosme-Llópez, and Jan J. M. M. Rutten. Regular varieties of automata and coequations. In MPC, pages 224-237, 2015. URL: https://doi.org/10.1007/978-3-319-19797-5_11.
  30. Julian Salamanca, Marcello M. Bonsangue, and Jurriaan Rot. Duality of equations and coequations via contravariant adjunctions. In Ichiro Hasuo, editor, CMCS, pages 73-93, 2016. URL: https://doi.org/10.1007/978-3-319-40370-0_6.
  31. 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.
  32. Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Coequations, coinduction, and completeness, 2021. URL: http://arxiv.org/abs/2102.08286.
  33. Alexandra Silva. Kleene coalgebra. PhD thesis, Radboud University, Nijmegen, 2010. URL: https://hdl.handle.net/2066/83205.
  34. 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, 2020. URL: https://doi.org/10.1145/3371129.
  35. 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.
  36. Henning Urbat, Jirí Adámek, Liang-Ting Chen, and Stefan Milius. Eilenberg theorems for free. In MFCS, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.43.
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