## Verification of Relational Data-Centric Dynamic Systems with
External Services

**Babak Bagheri Hariri, Diego Calvanese, Giuseppe De Giacomo, Alin
Deutsch, and Marco Montali**
*Proc. of the 32nd ACM SIGACT SIGMOD SIGART Symp. on
Principles of Database Systems (PODS 2013).* 2013.

Data-centric dynamic systems are systems where both the process
controlling the dynamics and the manipulation of data are equally
central. We study verification of (first-order) mu-calculus
variants over relational data-centric dynamic systems, where data
are maintained in a relational database, and the process is
described in terms of atomic actions that evolve the database.
Action execution may involve calls to external services, thus
inserting fresh data into the system. As a result such systems are
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 and 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 ensures that every service call activation
generates new values that cannot be accumulated indefinitely.

@inproceedings{PODS-2013-dcds,
title = "Verification of Relational Data-Centric Dynamic Systems with
External Services",
year = "2013",
author = "Bagheri Hariri, Babak and Diego Calvanese and De Giacomo,
Giuseppe and Alin Deutsch and Marco Montali",
booktitle = "Proc. of the 32nd ACM SIGACT SIGMOD SIGART Symp. on
Principles of Database Systems (PODS 2013)",
pages = "163--174",
doi = "10.1145/2463664.2465221",
}

pdf
url