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.

Intermediate reversed Moore machine | Minimal Moore machine |
---|---|

Determinised reachable automaton | Final partition |
---|---|

HKC | AC | HK |
---|---|---|

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

http://perso.ens-lyon.fr/damien.pous/brz/ Last modified: Wed Apr 17 11:58:45 CEST 2013