12 Search Results for "Brunet, Paul"


Document
Completeness Theorems for Kleene Algebra with Top

Authors: Damien Pous and Jana Wagemaker

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events.

Cite as

Damien Pous and Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{pous_et_al:LIPIcs.CONCUR.2022.26,
  author =	{Pous, Damien and Wagemaker, Jana},
  title =	{{Completeness Theorems for Kleene Algebra with Top}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.26},
  URN =		{urn:nbn:de:0030-drops-170890},
  doi =		{10.4230/LIPIcs.CONCUR.2022.26},
  annote =	{Keywords: Kleene algebra, Hypotheses, Completeness, Closed languages}
}
Document
Partially Observable Concurrent Kleene Algebra

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

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


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

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-dev.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
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra

Authors: Paul Brunet and David Pym

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


Abstract
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.

Cite as

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-dev.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
A Complete Axiomatisation of a Fragment of Language Algebra

Authors: Paul Brunet

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


Abstract
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.

Cite as

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-dev.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
Invited Talk
An Algebraic Framework to Reason About Concurrency (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency. The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi [Tobias Kappé et al., 2017; Tobias Kappé et al., 2019; Kappé et al., 2018]. Additional references can be found on the CoNeCo project website: https://coneco-project.org/.

Cite as

Alexandra Silva. An Algebraic Framework to Reason About Concurrency (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.FSTTCS.2019.6,
  author =	{Silva, Alexandra},
  title =	{{An Algebraic Framework to Reason About Concurrency}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{6:1--6:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.6},
  URN =		{urn:nbn:de:0030-drops-115687},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.6},
  annote =	{Keywords: Kleene Algebra, Concurrency, Automata}
}
Document
Kleene Algebra with Observations

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

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


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

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-dev.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
A Kleene Theorem for Nominal Automata (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Paul Brunet and Alexandra Silva

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


Abstract
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.

Cite as

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-dev.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
Reversible Kleene lattices

Authors: Paul Brunet

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


Abstract
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.

Cite as

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-dev.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
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

Authors: Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi

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


Abstract
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.

Cite as

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-dev.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
On Decidability of Concurrent Kleene Algebra

Authors: Paul Brunet, Damien Pous, and Georg Struth

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


Abstract
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.

Cite as

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-dev.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
Invited Talk
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)


Abstract
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 talk will overview why the problem is so difficult. We will then pave the way towards a solution, by presenting a new automaton model and a Kleene-like theorem for CKA. More precisely, we connect 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. We also survey how the present work can be used to to extend the network specification language NetKAT with primitives for concurrency so as to model and reason about concurrency within networks. This is joint work with Tobias Kappe, Paul Brunet, Bas Luttik, and Fabio Zanasi.

Cite as

Alexandra Silva. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.FSCD.2017.3,
  author =	{Silva, Alexandra},
  title =	{{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.3},
  URN =		{urn:nbn:de:0030-drops-77445},
  doi =		{10.4230/LIPIcs.FSCD.2017.3},
  annote =	{Keywords: Kleene algebras, Pomset languages, concurrency, NetKAT}
}
Document
A Formal Exploration of Nominal Kleene Algebra

Authors: Paul Brunet and Damien Pous

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


Abstract
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.

Cite as

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-dev.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}
}
  • Refine by Author
  • 9 Brunet, Paul
  • 6 Silva, Alexandra
  • 3 Kappé, Tobias
  • 3 Pous, Damien
  • 3 Wagemaker, Jana
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Semantics and reasoning
  • 1 Theory of computation → Algebraic language theory
  • 1 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 4 Kleene algebra
  • 3 Automata
  • 3 Concurrent Kleene algebra
  • 3 axiomatisation
  • 2 Concurrency
  • Show More...

  • Refine by Type
  • 12 document

  • Refine by Publication Year
  • 4 2017
  • 3 2019
  • 3 2020
  • 1 2016
  • 1 2022

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