Home » Events » Colloquium by Babak Hariri

# Colloquium by Babak Hariri

TITLE: Borders of Decidability in Verification of Data-Centric Dynamic Systems
SPEAKER: Babak Hariri, Free University of Bolzano

ABSTRACT: In this talk I present our recent results on data-aware static
verification, in which we select the artifact-centric model as a
natural vehicle for our investigation. Artifact-centric systems are
models for business process systems in which the dynamics and the
manipulation of data are equally central. Given the family of
variations on this model found in the literature, for the sake of a
uniform terminology we introduce our own pristine formalization, which
captures existing artifact-centric dialects, and which is semantically
equivalent to the most expressive ones. We call our business process
formalism Data-Centric Dynamic Systems'' (DCDS). The process is
described in terms of atomic actions that evolve the system. 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. More specifically, we
show that in a first-order $\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. Then, 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. We believe that DCDSs are natural and expressive models