Variable automata over infinite alphabets
=========================================
Automated reasoning about systems with infinite domains requires an
extension of regular automata to {\em infinite alphabets}. Existing
formalisms of such automata cope with the infiniteness of the alphabet
by adding to the automaton a set of registers or pebbles, or by
attributing the alphabet by labels from an auxilary finite alphabet
that is read by an intermediate transducer. These formalisms involve
a complicated mechanism on top of the transition function of automata
over finite alphabets and are therefore difficult to understand and to
work with.
We introduce and study {\em variable finite automata over infinite
alphabets} (VFA). VFA forms a natural and simple extension of regular
(and $\omega$-regular) automata, in which the alphabet consists of
letters as well as variables that range over the infinite alphabet
domain. Thus, VFAs have the same structure as regular automata, only
that some of the transitions are labeled by variables. We compare VFA
with existing formalisms, and study their closure properties and
classical decision problems. We consider the settings of both finite
and infinite words. In addition, we identify and study the
deterministic fragment of VFA. We show that while this fragment is
sufficiently strong to express many interesting properties, it is
closed under union, intersection, and complementation, and its
nonemptiness and containment problems are decidable. Finally, we
describe a determinization process for a determinizable subset of VFA.