Доклад представляет новые результаты теоретической информатики в области верификации параллельных и распределенных программ. Верификация — это процесс проверки выполнения требований к поведению программной системы на всех возможных траекториях ее вычислений. Недавний революционный прорыв в области верификации связан с методом Model checking (проверка модели), который состоит в том, что истинность формулы темпоральной логики, описывающей требование к поведению программы, проверяется на модели программы.

Темпоральная логика — это модальная логика, позволяющая формализовать утверждения о поведении дискретных систем, истинность которых зависит от времени. В докладе рассматривается логика ветвящегося времени CTL* и ее подклассы — логики CTL и LTL. Темпоральные логики оказались удобным формализмом для задания свойств корректного поведения дискретных систем, взаимодействующих друг с другом и окружением. Истинность либо ложность формул этих логик определяется на структуре Крипке — одном из формализмов, описывающих реактивные (реагирующие) систем с конечным числом состояний. Структура Крипке К называется “моделью” темпоральной формулы Ф, если Ф истинна на К. В докладе рассматриваются алгоритмы Model checking, т.е. алгоритмы проверки выполнимости темпоральных формул на структурах Крипке.