Document

**Published in:** LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

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.

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)

Copy BibTex To Clipboard

@InProceedings{wagemaker_et_al:LIPIcs.CONCUR.2020.20, author = {Wagemaker, Jana and Brunet, Paul and Docherty, Simon and Kapp\'{e}, Tobias and Rot, Jurriaan and Silva, Alexandra}, title = {{Partially Observable Concurrent Kleene Algebra}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {20:1--20:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.20}, URN = {urn:nbn:de:0030-drops-128324}, doi = {10.4230/LIPIcs.CONCUR.2020.20}, annote = {Keywords: Concurrent Kleene algebra, Kleene algebra with tests, observations, axiomatisation, completeness, sequential consistency} }

Document

**Published in:** LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, "pomset logic", that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. In contrast with other approaches, this logic is not state-based, but rather characterizes the runtime behaviour of a program. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.

Paul Brunet and David Pym. Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.FSCD.2020.8, author = {Brunet, Paul and Pym, David}, title = {{Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.8}, URN = {urn:nbn:de:0030-drops-123308}, doi = {10.4230/LIPIcs.FSCD.2020.8}, annote = {Keywords: Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules} }

Document

**Published in:** LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.

Paul Brunet. A Complete Axiomatisation of a Fragment of Language Algebra. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{brunet:LIPIcs.CSL.2020.11, author = {Brunet, Paul}, title = {{A Complete Axiomatisation of a Fragment of Language Algebra}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {11:1--11:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.11}, URN = {urn:nbn:de:0030-drops-116546}, doi = {10.4230/LIPIcs.CSL.2020.11}, annote = {Keywords: Kleene algebra, language algebra, completeness theorem, axiomatisation} }

Document

**Published in:** LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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.

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)

Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2019.41, author = {Kapp\'{e}, Tobias and Brunet, Paul and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio}, title = {{Kleene Algebra with Observations}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {41:1--41:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.41}, URN = {urn:nbn:de:0030-drops-109431}, doi = {10.4230/LIPIcs.CONCUR.2019.41}, annote = {Keywords: Concurrent Kleene algebra, Kleene algebra with tests, free model, axiomatisation, decision procedure} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Nominal automata are a widely studied class of automata designed to recognise languages over infinite alphabets. In this paper, we present a Kleene theorem for nominal automata by providing a syntax to denote regular nominal languages. We use regular expressions with explicit binders for creation and destruction of names and pinpoint an exact property of these expressions - namely memory-finiteness - identifying a subclass of expressions denoting exactly regular nominal languages.

Paul Brunet and Alexandra Silva. A Kleene Theorem for Nominal Automata (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 107:1-107:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.ICALP.2019.107, author = {Brunet, Paul and Silva, Alexandra}, title = {{A Kleene Theorem for Nominal Automata}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {107:1--107:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.107}, URN = {urn:nbn:de:0030-drops-106834}, doi = {10.4230/LIPIcs.ICALP.2019.107}, annote = {Keywords: Kleene Theorem, Nominal automata, Bracket Algebra} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

We investigate the equational theory of reversible Kleene lattices, that is algebras of languages with the regular operations (union, composition and Kleene star), together with intersection and mirror image. Building on results by Andréka, Mikulás and Németi from 2011, we construct the free representation of this algebra. We then provide an automaton model to compare representations. These automata are adapted from Petri automata, which we introduced with Pous in 2015 to tackle a similar problem for algebras of binary relations. This allows us to show that testing the validity of
equations in this algebra is decidable, and in fact ExpSpace-complete.

Paul Brunet. Reversible Kleene lattices. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brunet:LIPIcs.MFCS.2017.66, author = {Brunet, Paul}, title = {{Reversible Kleene lattices}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {66:1--66:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.66}, URN = {urn:nbn:de:0030-drops-81334}, doi = {10.4230/LIPIcs.MFCS.2017.66}, annote = {Keywords: Kleene algebra, Automata, Petri nets, Decidability, Complexity, Formal languages, Lattice} }

Document

**Published in:** LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.

Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2017.25, author = {Kapp\'{e}, Tobias and Brunet, Paul and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, title = {{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {25:1--25:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.25}, URN = {urn:nbn:de:0030-drops-77913}, doi = {10.4230/LIPIcs.CONCUR.2017.25}, annote = {Keywords: Kleene theorem, Series-rational expressions, Automata, Brzozowski derivatives, Concurrency, Pomsets} }

Document

**Published in:** LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Concurrent Kleene algebras support equational reasoning about
computing systems with concurrent behaviours. Their natural
semantics is given by series(-parallel) rational pomset languages, a
standard true concurrency semantics, which is often associated with
processes of Petri nets. We use constructions on Petri nets to
provide two decision procedures for such pomset languages motivated
by the equational and the refinement theory of concurrent Kleene
algebra. The contribution to the first problem lies in a much
simpler algorithm and an EXPSPACE complexity bound. Decidability
of the second, more interesting problem is new and, in fact,
EXPSPACE-complete.

Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.CONCUR.2017.28, author = {Brunet, Paul and Pous, Damien and Struth, Georg}, title = {{On Decidability of Concurrent Kleene Algebra}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {28:1--28:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.28}, URN = {urn:nbn:de:0030-drops-77881}, doi = {10.4230/LIPIcs.CONCUR.2017.28}, annote = {Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets} }

Document

**Published in:** LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

An axiomatisation of Nominal Kleene Algebra has been proposed by Gabbay and Ciancia, and then shown to be complete and decidable by Kozen et al. However, one can think of at least four different formulations for a Kleene Algebra with names: using freshness conditions or a presheaf structure (types), and with explicit permutations or not. We formally show that these variations are all equivalent.
Then we introduce an extension of Nominal Kleene Algebra, motivated by relational models of programming languages. The idea is to let letters (i.e., atomic programs) carry a set of names, rather than being reduced to a single name. We formally show that this extension is at least as expressive as the original one, and that it may be presented with or without a presheaf structure, and with or without syntactic permutations. Whether this extension is strictly more
expressive remains open.
All our results were formally checked using the Coq proof assistant.

Paul Brunet and Damien Pous. A Formal Exploration of Nominal Kleene Algebra. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 22:1-22:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.MFCS.2016.22, author = {Brunet, Paul and Pous, Damien}, title = {{A Formal Exploration of Nominal Kleene Algebra}}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)}, pages = {22:1--22:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-016-3}, ISSN = {1868-8969}, year = {2016}, volume = {58}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.22}, URN = {urn:nbn:de:0030-drops-64379}, doi = {10.4230/LIPIcs.MFCS.2016.22}, annote = {Keywords: Nominal sets, Kleene algebra, equational theory, Coq} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail