Data words

A data word is a word that is annotated with data values. Every position in a data word has the usual label from a finite alphabet, but it also has a label from an infinite set. Access to the second coordinate - called the data value - is restricted. We present a decidable automaton model for data words. Interestingly enough, this model reaches far beyond regular languages: emptiness for our automata is equivalent to reachability in Petri nets. We also present a decidable logic for reasoning about data words, this is a type of two-variable first-order logic.