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

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