A package containing various properties checkers on automaton objects, mainly simple unary tests and equivalence relations.

Documentation

This package offers the following unary tests on automaton:
emptiness:
checks if given automaton is empty
normalized:
checks if automaton as one start state with no incoming transitions and one end state,
contains epsilon:
checks if the automaton recognizes the empty word epsilon,
It also offers an extensible framework for computing equivalence relations over automata. The {@see rationals.properties.AreEquivalent} class checks that starting states of both automata are equivalent according to some {@see rationals.properties.Relation}. Predefined relation objects are;
Completed Trace equivalence:
compute the equivalence of two states according to the language they recognize,
Weak Bisimulation:
checks that two states produces the same labels and lead to equivalent states, without taking into account epsilon transitions,
(Strong) Bisimulation:
checks that two states produces the same labels and lead to equivalent states, epsilon transitions are accounted for.
Isomorphism:
checks that two automaton are isomorph up to a renaming of states.
Obviously, these equivalence relations are meaningful only when one does not want to compute the minimal DFA for a given automaton as in this case they all collapse into (completed) trace equivalence.