Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке - Чеботарев, А.Н. (Кибернетика и системный анализ, 2009)
Розглянуто методи верифікації специфікацій реактивних алгоритмів у мові L. Верифікація здійснюється відносно властивостей, поданих у вигляді формул класу GR(1) темпоральної логіки LTL, і зводиться до перевірки виконуваності формул у мові L