# Concurrent Kleene Algebra

## Software : CKA

Bitbucket repository.

Some online applications are also available below.

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

## Details of the checking of an inequation

 ≤

 Net for the first expression: Net for the second expression: Automaton of the accepting runs: Product automaton: