Décider si deux automates reconnaissent le même langage se fait sans essayer le moindre mot : il suffit de les minimiser et de comparer les résultats.
Objectif
Nommer ce que la méthode exige et ce qu'elle garantit.
Ce qui fonde la méthode
L'automate minimal d'un langage est unique, au renommage des états près. Deux automates reconnaissent donc le même langage si et seulement si leurs minimaux coïncident. Quand ils ne coïncident pas, le raffinement ne se contente pas de dire non : il indique la classe où la divergence est apparue, et la suite de symboles qui y mène est un mot accepté par l'un et refusé par l'autre. Une preuve de différence tient donc en un seul mot, et c'est ce mot qu'on écrit dans un rapport plutôt qu'une affirmation.