Verification of Relational Data-Centric Dynamic Systems with External Services

TL;DR

This paper investigates the verification of relational data-centric dynamic systems with external services, identifying conditions under which the verification problem remains decidable despite the systems' inherent infinite-state nature.

Contribution

It introduces novel decidability results for verifying such systems by analyzing specific service call behaviors and data accumulation constraints, including the concept of generate-recall acyclicity.

Findings

Decidability achieved for systems with deterministic service calls and bounded fresh data.

Decidability established for systems with nondeterministic services under certain knowledge preservation conditions.

Introduction of generate-recall acyclicity to prevent infinite data accumulation and ensure verification feasibility.

Abstract

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.