joint work with Luc Segoufin

In this paper we work over linearly ordered data domains
equipped with finitely many unary predicates and constants. We consider
nondeterministic automata processing words and storing finitely many
variables ranging over the domain. During a transition, these automata
can compare the data values of the current configuration with those of
the previous configuration using the linear order, the unary predicates
and the constants. We show that emptiness for such automata is decidable, both over finite
and infinite words, under reasonable computability assumptions on the
linear order. Finally, we show how our automata model can be used for verifying
properties of workflow specifications in the presence of an underlying
database.