  Data-centric dynamic systems are systems where both the process controlling
the dynamics and the manipulation of data are equally central. In this paper we
study verification of (first-order) mu-calculus variants over relational
data-centric dynamic systems, where data are represented by a full-fledged
relational database, and the process is described in terms of atomic actions
that evolve the database. The execution of such actions may involve calls to
external services, providing fresh data inserted into the system. As a result
such systems are typically infinite-state. We show that verification is
undecidable in general, and we isolate notable cases, where decidability is
achieved. Specifically we start by considering service calls that return values
deterministically (depending only on passed parameters). We show that in a
mu-calculus variant that preserves knowledge of objects appeared along a run we
get decidability under the assumption that the fresh data introduced along a
run are bounded, though they might not be bounded in the overall system. In
fact we tie such a result to a notion related to weak acyclicity studied in
data exchange. Then, we move to nondeterministic services where the assumption
of data bounded run would result in a bound on the service calls that can be
invoked during the execution and hence would be too restrictive. So we
investigate decidability under the assumption that knowledge of objects is
preserved only if they are continuously present. We show that if infinitely
many values occur in a run but do not accumulate in the same state, then we get
again decidability. We give syntactic conditions to avoid this accumulation
through the novel notion of "generate-recall acyclicity", which takes into
consideration that every service call activation generates new values that
cannot be accumulated indefinitely.
