Анотація. Розглянуто два фрагменти, LP і LF, логіки першого порядку з обмеженими кванторами, які використовуються для специфікації трансд’юсерів. Логіка LP дозволяє характеризувати поточну поведінку системи на основі її минулої поведінки, а LF — на основі майбутньої поведінки. Визначено два види семантик для цих логік та досліджено властивості автоматів, що в них специфікуються.

Ключові слова: логіки першого порядку, формули минулого часу, формули майбутнього часу, автоматна семантика, симетричні формули.