метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить удовлетворяет ли заданная модель системы формальным спецификациям.
В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: {\displaystyle M=\left(S,S_{0},R,L\right)} M = \left(S, S_0, R, L\right) , где {\displaystyle S} S — множество состояний, {\displaystyle S_{0}} S_{0} — множество начальных состояний, {\displaystyle R\subseteq S\times S} R \subseteq S \times S — отношение переходов, {\displaystyle L:S\rightarrow 2^{AP}} L: S \rightarrow 2^{AP} — функция разметки.
бинаторного взрыва в пространстве состояний. Эта проблема возникает в системах, состоящих из многих компонентов, взаимодействующих друг с другом, а также в системах, обладающих структурами данных, способных принимать большое число значений.