Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем - Колчин, А.В. (Искусственный интеллект, 2013)
В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании доказательства изоморфизма на графе информационных зависимостей модели. Во многих случаях такой подход существенно сокращает эффект «комбинаторного взрыва» количества состояний.