Related documents |
Software : CKA |
Some online applications are also available below.
Papers |
[-] |
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.
@techreport{brunet19-2019, institution={}, title="Kleene Algebra with Observations", year={2019}, author={Brunet, Paul and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio} }
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, journal={JLAMP}, title="On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata", year={2019}, url={https://doi.org/10.1016/j.jlamp.2018.12.001}, author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio} }
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, journal={LMCS}, title="Equivalence checking for weak bi-Kleene algebra", year={2018}, note={submitted}, author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio} }
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, booktitle={ESOP}, title="Concurrent Kleene Algebra: Free Model and Completeness", year={2018}, url={https://doi.org/10.1007/978-3-319-89884-1_30}, author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Zanasi, Fabio} }
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, booktitle={CONCUR}, title="On Decidability of Concurrent Kleene Algebra", year={2017}, url={http://drops.dagstuhl.de/opus/volltexte/2017/7788/}, author={Brunet, Paul and Pous, Damien and Struth, Georg} }
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, booktitle={CONCUR}, title="Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages", year={2017}, url={http://drops.dagstuhl.de/opus/volltexte/2017/7791/}, author={Brunet, Paul and Kappé, Tobias and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio} }
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: | |