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