Related documents |
Software : CKA |
Some online applications are also available below.
Papers |
[-] |
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate 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.
@inproceedings{brunet25-2020, title="Partially Observable Concurrent Kleene Algebra", author={Brunet, Paul and Docherty, Simon and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana}, year={2020}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2020.20"}, }
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 protect 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 pratical purposes. We provide a logic, ‘pomset logic’, that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. We develop the basic metatheory for the relationship between pomset logic and CKA and illustrate this relationship with simple examples.
@inproceedings{brunet22-2020, title="Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra", author={Brunet, Paul and Pym, David}, year={2020}, booktitle={FSCD}, doi={"10.4230/LIPIcs.FSCD.2020.8"}, }
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditional and while-loops. It turns out integrating tests in CKA is subtle, due to their interaction with parallel threads. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.
@inproceedings{brunet21-2020, title="Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness", author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio}, year={2020}, booktitle={FoSSaCS}, doi={"10.1007/978-3-030-45231-5_20"}, }
Kleene algebra with tests (KAT) gives an algebraic perspective on reasoning about the control flow of sequential programs. However, when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with axioms for reasoning about concurrency lead to a bizarre 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.
@inproceedings{brunet19-2019, title="Kleene Algebra with Observations", author={Brunet, Paul and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio}, year={2019}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2019.41"}, }
Concurrent Kleene Algebra (CKA) is a formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, an important tool to develop foundations and potential applications is a one-to- one correspondence between denotational and operational perspectives. This paper takes an important step towards such a correspondence, by precisely relating Bi-Kleene Algebra (BKA), a relaxed version of CKA, to a novel type of automata called pomset automata. We show that pomset automata can faithfully represent the BKA-semantics of series-parallel rational expressions, and that a (structurally restricted) class of pomset automata can be translated back to these expressions. Furthermore, we characterise the behavior of unrestricted automata in terms of context-free pomset grammars, thus yielding strong undecidability results.
@article{brunet15-2019, title="On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2019}, journal={JLAMP}, doi={"10.1016/j.jlamp.2018.12.001"}, }
Pomset automata are an operational model of weak bi-Kleene algebra, which describes program that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.
@article{brunet16-2018, title="Equivalence checking for weak bi-Kleene algebra", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2018}, journal={LMCS}, note={submitted}, }
Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the semantics proposed in the original paper is the free model of CKA with bounded parallel iteration, meaning the completeness of these axioms. This result settles a conjecture of Hoare and collaborators. Moreover, it allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.
@inproceedings{brunet14-2018, title="Concurrent Kleene Algebra: Free Model and Completeness", author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Zanasi, Fabio}, year={2018}, booktitle={ESOP}, doi={"10.1007/978-3-319-89884-1_30"}, }
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.
@inproceedings{brunet13-2017, title="On Decidability of Concurrent Kleene Algebra", author={Brunet, Paul and Pous, Damien and Struth, Georg}, year={2017}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2017.28"}, }
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 for 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.
@inproceedings{brunet11-2017, title="Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages", author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio}, year={2017}, booktitle={CONCUR}, doi={"10.4230/LIPIcs.CONCUR.2017.25"}, }
Talks |
[-] |
Documents |
[-] |
Syntax for expressions and equations |
Equations should be entered like this:
<expr1> <cmp> <expr2>
.
An expression can use strings as variables/letters, and the operations:
0
: the empty set;1
: the empty process;<expr1> + <expr2>
: the set
union;<expr1> | <expr2>
: the parallel
product;<expr1> . <expr2>
: the sequential
product;<expr1>^+
: the transitive closure;<expr1>^*
: the reflexive transitive
closure;<expr1>{int}
: the iteration. For
instance, (a.b){3}
is a shorthand
for (a.b).(a.b).(a.b)
.You can also use brackets (...)
. The valid
comparaisons <cmp>
are:
<=
: loose inclusion
>=
: converse of the loose inclusion
<
: strict inclusion
>
: converse of the strict inclusion
=
: equality
=/=
: negation of the equality
<>
: means that the two expressions are
incomparable,
i.e. neither one of them is included in the
other.
For instance,
(a|b)^+.C + d < d + a.b.C + (d|a)
is an acceptable equation.
Test equations |
View the net associated with an expression |
Details of the checking of an inequation |
≤ |
Net for the first expression: | Net for the second expression: | |
Automaton of the accepting runs: | Product automaton: | |