Конечный автомат может быть использован как модель для описания и анализа поведения дискретных систем. В этой статье предлагается приближённый алгоритм проверки эквивалентности двух расширенных конечных автоматов, основанный на понятии предикатной абстракции. Также проводится экспериментальная оценка схожести расширенного конечного автомата и его предикатной абстракции.
