Campus Event Calendar

Event Entry

New for: D1, D2, D3, D4, D5

What and Who

Borders of Decidability in Verification of Data-Centric Dynamic Systems

Babak Bagheri
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience

Date, Time and Location

Thursday, 14 February 2013
60 Minutes


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 for systems powered by an underlying database (i.e., so called data-centric systems), and thus are an ideal vehicle for foundational research with potential to transfer to alternative models.


Susanne Rock
--email hidden

Video Broadcast

E1 5
passcode not visible
logged in users only

Susanne Rock, 02/21/2013 09:13
Susanne Rock, 02/15/2013 14:43 -- Created document.