Logo Concurrent Kleene Algebra

Software : CKA

Bitbucket repository.

Documentation.

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.

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: