Document Open Access Logo

Partially Observable Concurrent Kleene Algebra

Authors Jana Wagemaker , Paul Brunet , Simon Docherty , Tobias Kappé , Jurriaan Rot, Alexandra Silva

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2020.20.pdf
  • Filesize: 0.62 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Concurrency
  • Theory of computation → Formal languages and automata theory
Keywords
  • Concurrent Kleene algebra
  • Kleene algebra with tests
  • observations
  • axiomatisation
  • completeness
  • sequential consistency

Metrics

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

Abstract

We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with variables as well as control structures, such as conditionals and loops, that depend on those variables. We illustrate the use of POCKA through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

Cite As Get BibTex

Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva. Partially Observable Concurrent Kleene Algebra. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.20

Author Details

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

Funding

ERC Starting Grant ProFoundNet (679127).
  • Brunet, Paul: EPSRC grant IRIS (EP/R006865/1).
  • Docherty, Simon: EPSRC grant (EP/S013008/1).

References

  1. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Litmus: Running tests against hardware. In TACAS, pages 41-44, 2011. URL: https://doi.org/10.1007/978-3-642-19835-9_5.
  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. Thomas S. Blyth. Lattices and Ordered Algebraic Structures. Springer-Verlag London, 2005. Google Scholar
  4. John Horton Conway. Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London, 1971. Google Scholar
  5. 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.
  6. 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.
  7. 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.
  8. Jan Grabowski. On partial languages. Fundam. Inform., 4(2):427, 1981. Google Scholar
  9. 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.
  10. 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.
  11. Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene algebra with observations. In CONCUR, pages 41:1-41:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.41.
  12. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene algebra with observations: From hypotheses to completeness. In FOSSACS, pages 381-400, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  13. 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.
  14. 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.
  15. 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.
  16. Daniel Krob. A complete system of B-rational identities. In ICALP, pages 60-73, 1990. URL: https://doi.org/10.1007/BFb0032022.
  17. Leslie Lamport. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Computers, 46(7):779-782, 1997. URL: https://doi.org/10.1109/12.599898.
  18. 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.
  19. Kamal Lodaya and Pascal Weil. Series-parallel languages and the bounded-width property. Theoretical Computer Science, 237(1):347-380, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00031-1.
  20. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LiCS, July 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  21. 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.
  22. Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva. Partially observable concurrent Kleene algebra, 2020. URL: http://arxiv.org/abs/2007.07593.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact