Некоторые подмножества монадической логики первого порядка (MFO), используемые для спецификации и синтеза ∑-автоматов

Abstract

Рассмотрены два фрагмента, LP и LF, логики первого порядка с ограниченными кванторами, используемые для спецификации трансдьюсеров. Логика LP позволяет характеризовать текущее поведение системы на основе ее поведения в прошлом, а LF — на основе поведения в будущем. Определены два вида семантик для этих логик и исследованы свойства специфицируемых в них автоматов.Розглянуто два фрагменти, LP і LF, логіки першого порядку з обмеженими кванторами, які використовуються для специфікації трансд’юсерів. Логіка LP дозволяє характеризувати поточну поведінку системи на основі її минулої поведінки, а LF — на основі майбутньої поведінки. Визначено два види семантик для цих логік та досліджено властивості автоматів, що в них специфікуються.Two fragments, LP and LF, of first-order logic with bounded quantifiers used for specification of transducers are considered. Fragment LP enables the current behaviour of a system to be characterized on the basis of its past behaviour, and LF relies on the future behaviour. Two kinds of semantics are defined for logics LP and LF, and the properties of automata specified in these logics are investigated.