CKA : Concurrent Kleene Algebras
Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. This project concerns itself with the study of this framework, and of its enhancements with extra features. The aim is to carry out sophisticated verification tasks using this language.
Test equations
How to use this :
Write an equation in the input field of the applet, and see its validity just to the right (a green tick meaning yes and a red cross meaning no).
Equations should be entered like this:
<expr1> <cmp> <expr2>
An expression can use strings as variables/letters, and the operations:
0: the empty set1: the empty process<expr1> + <expr2>: the set union<expr1> | <expr2>: the parallel product<expr1> . <expr2>: the sequential product<expr1>*: the unbounded sequential iteration<expr1>+: the unbounded non-empty sequential iteration<expr1>{<int>}: the fixed 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.
The tester
Net viewer
Detailled equation checking
| ≤ |
| Net for the first expression: | Net for the second expression: | |
| Automaton of the accepting runs: | Product automaton: | |