Brzozowski's minimisation and bisimulations up-to for for must testing

- Filippo Bonchi
- Georgiana Caltais
- Damien Pous
- Alexandra Silva
Input LTS
Brzozowski's minimisation
Determinisation + PR

This page is a web-appendix to a paper where we generalize Brzozowski's minimisation algorithm, and variants of Hopcroft and Karp's algorithm for the language equivalence of NFA, to various decorated trace semantics, including must testing.

The applet below make it possible to execute the various algorithms on concrete labelled transition systems (LTS): it suffices to type the LTS in the textbox below (see the precise syntax at the end of this page).

Note that the failure sets are displayed using the more compact antichain representation. (For instance with two letters a and b, the antichain {{a}} denotes the failure set {{},{b}}, the antichain {{a},{b}} denotes the failure set {{},{a},{b}}, and the antichain {{a,b}}} denotes the failure set {{}}.)

The states to start the minimisation with are specified using the "start:" keyword, while the states to compare using bisimulations up-to algorithms are specified using the "check:" keyword.

Enter your automaton here Summary (-) Decorated weak automaton (-) Strong similarity

(-) Brzozowski's minimisation

Intermediate reversed Moore machine Minimal Moore machine

(-) Determinisation + Partition Refinement minimisation

Determinised reachable automaton Final partition

(-) Bisimulations up-to for (in)equivalence



// adding transitions (states can be arbitrary non-empty words, labels can be regular expressions):
x -a-> y
y -b-> y1
y -tau-> y1 // silent label is called tau
u -a-> v v' // adds transitions to v and v'
u u' -a-> v // adds transitions from u and u'
u -a+b-> v // adds transitions with labels a and b
u -a^*.b-> v // adds a transition with a regular expression a^*.b

// specifying initial states to start minimisation with

start: x y z

// asking for a given inclusion or equality (only the last one is used)

check: x <= u v
check: x y = u
check: x y => u v
Last modified: Wed Apr 17 11:58:45 CEST 2013