Logo KAC : Kleene Algebras with Converse

Related Documents

Back to top

Equation checker

Back to top

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 relation
  • 1: the identity relation
  • <expr1> | <expr2>: the set union
  • <expr1> . <expr2>: the composition of relations
  • <expr1>~ : the converse of a relation
  • <expr1>*: the reflexive transitive closure of a relation.
  • <expr1>+: the transitive closure of a relation.
  • <expr1>{int} : the iteration of a relation. For instance, (a.b){3} is a shorthand for (a.b).(a.b).(a.b).

You can also use brackets (...). For letters/variables, you may use a' instead of a~. 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, ((1|a'|b)+|C)~.a=/=0 is an acceptable equation.



Automata builder

Back to top

How to use this :

Simply input an automaton in the text box, choose from one of the constructions on the left scroll box, and click "Build" to generate the automaton and its closure.

An automaton is specified through the following syntax:

initial : <list of initial states separated by spaces>
final : <list of final states separated by spaces>
<source> -- <label> --> <target>
<source> -- <label> --> <target>

See below for an example.


Initial automaton:
Closure automaton:

The KAC suite

Back to top
KAC is an OCaml solution for manipulating automata and and deciding the theories KACl and KAC.
  • The sources can be downloaded from here.
  • The documentation is available online here.