Верификация синхронно-автоматных программ с использованием LTL

Предлагается способ верификации синхронно-автоматных программ с использованием языка линейной темпоральной логики с операторами прошедшего времени. Исследуется использование программного инструмента TempEst. Описание и проверка свойств демонстрируются на примере часов с будильником.