LIPIcs.CONCUR.2020.20.pdf
- Filesize: 0.62 MB
- 22 pages
Document
Partially Observable Concurrent Kleene Algebra
Authors
Jana Wagemaker 
,
Paul Brunet ,
Simon Docherty ,
Tobias Kappé ,
Alexandra Silva
-
Part of:
Volume:
31st International Conference on Concurrency Theory (CONCUR 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-08-26
File
Document Identifiers
Author Details
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
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.
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)
0PDF Downloads
References
- 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.
- 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.
-
Thomas S. Blyth. Lattices and Ordered Algebraic Structures. Springer-Verlag London, 2005.
-
John Horton Conway. Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London, 1971.
- 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.
- 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.
- 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.
-
Jan Grabowski. On partial languages. Fundam. Inform., 4(2):427, 1981.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Daniel Krob. A complete system of B-rational identities. In ICALP, pages 60-73, 1990. URL: https://doi.org/10.1007/BFb0032022.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.