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

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.

(-) Brzozowski's minimisation

(-) Determinisation + Partition Refinement minimisation

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

Syntax

// 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

---

http://perso.ens-lyon.fr/damien.pous/brz/

Last modified: Wed Apr 17 11:58:45 CEST 2013