Abstract. 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.

Keywords: first order logics, past formulas, future formulas, automatic semantics, symmetric formulas.