Attributed automata (AA) were introduced by M.Meriste and J.Penjam as a formalism for executable specifications using regular syntax with attributes representing contextual relations as well as semantic properties of underlying concepts. Due to applications in medical signal analysis AA is accepted as a software engineering tool.
This year, a functional specification method for attributed automata was developed, which has good compositional properties.
The functioning of the transformational automaton is analoguous to the
case of finite attributed automata: it starts from the initial state
with the initial attribute value 
. A
transition from one state two another is possible only if the
corresponding enabling predicate is true. The transition is
accompanied by avaluation of the attribute of the next state using the
associated transformation function. The automaton stops if there is no
transitions enabled. If this happens in the final state 
, then
the automaton finished successfully and the current value of the
attribute 
is treated as the output of automaton.
This situation is denoted by 
. If automaton stops in
some other state or doesn't stop at all, then the automaton fails and
this is denoted by 
. This explains why such
automata are called transformational -- their only effect is the
transformation of inputs into outputs.
Example. AA can accept some context-sensitive languages. In Fig.1, the an automaton for the language 
. To model input string, the specialcomponent of attributes is used.
Figure: Recognizer of the language