В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании доказательства изоморфизма на графе информационных зависимостей модели.
