Document Open Access Logo

Kleene Algebra with Observations

Authors Tobias Kappé , Paul Brunet , Jurriaan Rot, Alexandra Silva , Jana Wagemaker, Fabio Zanasi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2019.41.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Concurrent Kleene algebra
  • Kleene algebra with tests
  • free model
  • axiomatisation
  • decision procedure

Metrics

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

Abstract

Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

Cite As Get BibTex

Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene Algebra with Observations. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.41

Author Details

Tobias Kappé
  • University College London, UK
Paul Brunet
  • University College London, UK
Jurriaan Rot
  • University College London, UK
  • Radboud University, Nijmegen, The Netherlands
Alexandra Silva
  • University College London, UK
Jana Wagemaker
  • University College London, UK
Fabio Zanasi
  • University College London, UK

Funding

ERC Starting Grant ProFoundNet (679127)
  • Rot, Jurriaan: Marie Curie Fellowship (795119)
  • Silva, Alexandra: Leverhulme Prize (PLP-2016-129)
  • Zanasi, Fabio: EPSRC grant (EP/R020604/1)

Acknowledgements

We are grateful to Jean-Baptiste Jeannin, Dan Frumin and Damien Pous individually, for their input which helped contextualise this work.

References

  1. 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.
  2. Valentin M. Antimirov. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theor. Comput. Sci., 155(2):291-319, 1996. URL: https://doi.org/10.1016/0304-3975(95)00182-4.
  3. Roland Backhouse. Closure algorithms and the star-height problem of regular languages. PhD thesis, University of London, 1975. Google Scholar
  4. Garrett Birkhoff and Thomas C. Bartee. Modern applied algebra. McGraw-Hill, 1970. Google Scholar
  5. Maurice Boffa. Une remarque sur les systèmes complets d'identités rationnelles. ITA, 24:419-428, 1990. Google Scholar
  6. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In POPL, pages 457-468, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  7. Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In CONCUR, pages 28:1-28:15, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.28.
  8. Janusz A. Brzozowski. Derivatives of Regular Expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  9. John Horton Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971. Google Scholar
  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. Jay L. Gischer. The Equational Theory of Pomsets. Theor. Comput. Sci., 61:199-224, 1988. URL: https://doi.org/10.1016/0304-3975(88)90124-7.
  12. Jan Grabowski. On partial languages. Fundam. Inform., 4(2):427, 1981. Google Scholar
  13. Tony Hoare. Laws of Programming: The Algebraic Unification of Theories of Concurrency. In CONCUR, pages 1-6, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_1.
  14. Tony Hoare, Ian J. Hayes, Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm Sørensen, J. Michael Spivey, and Bernard Sufrin. Laws of Programming. Commun. ACM, 30(8):672-686, 1987. URL: https://doi.org/10.1145/27651.27653.
  15. Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra. In CONCUR, pages 399-414, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_27.
  16. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, and Huibiao Zhu. Developments in Concurrent Kleene Algebra. J. Log. Algebr. Meth. Program., 85(4):617-636, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.09.012.
  17. John E. Hopcroft and Richard M. Karp. A linear algorithm for testing equivalence of finite automata. Technical Report TR71-114, Cornell University, December 1971. Google Scholar
  18. Bart Jacobs. A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages. In Algebra, Meaning, and Computation (Joseph A. Goguen festschrift), pages 375-404, 2006. URL: https://doi.org/10.1007/11780274_20.
  19. Peter Jipsen and M. Andrew Moshier. Concurrent Kleene algebra with tests and branching automata. J. Log. Algebr. Meth. Program., 85(4):637-652, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.12.005.
  20. Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene Algebra with Observations. CoRR, abs/1811.10401, 2018. URL: http://arxiv.org/abs/1811.10401.
  21. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent Kleene Algebra: Free Model and Completeness. In ESOP, pages 856-882, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_30.
  22. Stephen C. Kleene. Representation of Events in Nerve Nets and Finite Automata. Automata Studies, pages 3-41, 1956. Google Scholar
  23. Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inf. Comput., 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  24. 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.
  25. Dexter Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log., 1(1):60-76, 2000. URL: https://doi.org/10.1145/343369.343378.
  26. 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.
  27. Dexter Kozen and Konstantinos Mamouras. Kleene Algebra with Equations. In ICALP, pages 280-292, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_24.
  28. 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.
  29. 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.
  30. Daniel Krob. Complete Systems of B-Rational Identities. Theor. Comput. Sci., 89(2):207-343, 1991. URL: https://doi.org/10.1016/0304-3975(91)90395-I.
  31. Michael R. Laurence and Georg Struth. Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages. In RAMiCS, pages 65-82, 2014. URL: https://doi.org/10.1007/978-3-319-06251-8_5.
  32. Michael R. Laurence and Georg Struth. Completeness Theorems for Pomset Languages and Concurrent Kleene Algebras, 2017. URL: http://arxiv.org/abs/1705.05896.
  33. Kamal Lodaya and Pascal Weil. Series-parallel languages and the bounded-width property. Theor. Comput. Sci., 237(1):347-380, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00031-1.
  34. Damien Pous. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In POPL, pages 357-368, 2015. URL: https://doi.org/10.1145/2676726.2677007.
  35. Michael O. Rabin and Dana S. Scott. Finite Automata and Their Decision Problems. IBM J. of Research and Dev., 3(2):114-125, 1959. URL: https://doi.org/10.1147/rd.32.0114.
  36. Jurriaan Rot, Filippo Bonchi, Marcello M. Bonsangue, Damien Pous, Jan Rutten, and Alexandra Silva. Enhanced coalgebraic bisimulation. Mathematical Structures in Comput. Sci., 27(7):1236-1264, 2017. URL: https://doi.org/10.1017/S0960129515000523.
  37. Jan J. M. M. Rutten. Automata and Coinduction (An Exercise in Coalgebra). In CONCUR, pages 194-218, 1998. URL: https://doi.org/10.1007/BFb0055624.
  38. 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.
  39. 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.
  40. Alexandra Silva. Kleene Coalgebra. PhD thesis, Radboud Universiteit Nijmegen, 2010. Google Scholar
  41. Steffen Smolka, Spiridon Aristides Eliopoulos, Nate Foster, and Arjun Guha. A fast compiler for NetKAT. In ICFP, pages 328-341, 2015. URL: https://doi.org/10.1145/2784731.2784761.
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