  To model Web services handling data from an infinite domain, or with multiple
sessions, we introduce fresh-variable automata, a simple extension of
finite-state automata in which some transitions are labeled with variables that
can be refreshed in some specified states. We prove several closure properties
for this class of automata and study their decision problems. We then introduce
a notion of simulation that enables us to reduce the Web service composition
problem to the construction of a simulation of a target service by the
asynchronous product of existing services, and prove that this construction is
computable.
