PaperlayerView exact revision on arXiv

Source-linked AI summary

Verification of Relational Data-Centric Dynamic Systems with External Services

Babak Bagheri Hariri, Diego Calvanese, Giuseppe De Giacomo, Alin Deutsch, Marco Montali

arXiv:1203.0024v1cs.DB

TL;DR

The paper addresses verification of expressive first-order μ-calculus properties over relational data-centric dynamic systems, which are generally infinite-state because actions can obtain fresh external data. It develops logic-sensitive abstractions and identifies decidable boundedness regimes, while showing undecidability in general and distinguishing deterministic from nondeterministic service cases.

  • Problem

    Verification is difficult because relational DCDSs combine sophisticated process properties with potentially unbounded data and external services that introduce fresh values.

  • Method

    The paper studies μLA and μLP, defines bisimulation-based abstractions, and analyzes deterministic and nondeterministic services under run- or state-boundedness conditions.

  • Results

    Verification of both μLA and μLP is undecidable in general, while decidability is obtained for deterministic run-bounded systems and relevant nondeterministic state-bounded systems; the resulting verification complexity is in EXPTIME.

  • Takeaways & Limitations

    Deterministic and nondeterministic services have equivalent expressive power on unrestricted DCDSs but differ with respect to verification decidability under boundedness restrictions.

  • Takeaways & Limitations

    The decidability results are tied to restricted boundedness assumptions, and run-boundedness itself is undecidable to check.

Abstract

from arXiv · show

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.

1. INTRODUCTION

The paper studies verification of relational data-centric dynamic systems, where processes and evolving relational data are equally central and external services can introduce fresh values. It identifies general undecidability and decidable cases for two first-order μ-calculus variants under different service and data-boundedness assumptions.

  • Motivation: The verification challenge arises because unbounded data evolution defeats standard finite-state model checking while properties may require sophisticated temporal logics.Both data and process behavior must be analyzed simultaneously.
  • Motivation: Relational DCDSs combine a process layer with a full-fledged relational database whose evolution may involve external services returning fresh data.These features make the systems infinite-state in general.
  • Verification logics: The paper studies first-order μ-calculus variants that preserve knowledge either of objects appearing along a run or only of objects continuously present.These variants are respectively μLA and μLP.
  • Main results: Verification of both μLA and μLP is undecidable in general, even without first-order quantification and branching time.The paper therefore focuses on restricted decidable classes.
  • Main results: For deterministic services, μLA verification is decidable when fresh data are bounded along each run, with weak acyclicity providing a sufficient syntactic condition.Run-boundedness need not hold across all runs.
  • Main results: The paper then investigates nondeterministic services because run-boundedness would restrict how often same-argument service calls can occur.The introduction motivates a separate treatment of nondeterministic services.

2. DATA-CENTRIC DYNAMIC SYSTEMS

A DCDS consists of a relational data layer and a process layer that queries and updates it through actions, potentially invoking external services. Its semantics is a possibly infinite transition system whose database-labeled states capture all process computations.

  • System structure: A DCDS is formed by interacting data and process layers, with the data layer storing information and the process layer evolving it.The framework deliberately keeps both layers structurally minimal.
  • Data layer: The data layer contains a relational schema, equality constraints, and an initial database instance over a possibly infinite set of constants.The initial instance conforms to the schema and satisfies the constraints.
  • Data layer: The active domain ADOM(I) is the set of constants that occur in database instance I.This notion is used to characterize values currently present in a state.
  • Process layer: The process layer comprises actions, external services, and condition-action rules that query the current database and update it.Action effects can include service-generated Skolem terms representing externally supplied values.
  • Process layer: An action has input parameters and simultaneous effect specifications, whose queries and effects determine the next database contents.Effects may combine initial constants, parameters, query variables, and service calls.
  • Transition-system semantics: The semantics is a possibly infinite transition system with database-labeled states, an initial state, and transitions representing all computations of the process layer.Its infinite-state character reflects potentially unbounded data growth.

3. VERIFICATION

The paper uses first-order μ-calculus to verify dynamic properties of infinite-state DCDSs, then introduces restricted fragments and bisimulation notions supporting finite abstractions. The fragments differ in whether quantified objects must be currently present or persist across transitions.

  • μ-calculus: First-order μ-calculus combines first-order queries, modal transitions, and least or greatest fixpoints for expressing dynamic properties.Its fixpoint variables must satisfy syntactic monotonicity.
  • Verification challenge: The full logic is difficult to abstract finitely because the DCDS transition system is generally infinite-state and some formulas defeat finite-state abstractions.The paper therefore introduces two sublogics.
  • Restricted logics: μLA restricts individual quantification to values in the current active domain through the predicate LIVE(x), while preserving history-aware object correspondences.It supports formulas whose quantification ranges over currently present objects.
  • Bisimulation: History-preserving bisimulation uses partial bijections between data domains and extends those correspondences across matching transitions.This accounts for data that evolve over time in different transition systems.
  • Bisimulation: Theorem 3.1 states that history-preserving bisimilar transition systems agree on every closed μLA formula, while the analogous relation preserves every closed μLP formula.These results justify the corresponding abstractions for verification.
  • Restricted logics: μLP further requires quantified individuals to persist continuously along system evolution for the quantification to remain relevant.Its transition modality explicitly enforces persistence with LIVE conditions.

4. DETERMINISTIC SERVICES

With deterministic external services, the paper models DCDS states by databases plus remembered service-call results and studies verification through finite abstractions. Verification is undecidable in general, but becomes decidable for run-bounded systems and for weakly acyclic systems, with reduction to finite-state propositional µ-calculus model checking.

  • Service semantics: Deterministic services return the same value whenever called with the same parameters, so states retain prior service-call results.A concrete state is a database instance paired with a service call map.
  • Service semantics: Concrete execution applies guarded actions and their effects, updates the database, records service-call bindings, and enforces equality constraints.The transition construction includes legal parameter assignments, service-call processing, effect evaluation, and constraint satisfaction.
  • Undecidability: Verification is undecidable even for propositional LTL safety properties, and full µ-calculus lacks a faithful finite-state abstraction in general.The paper also identifies a µ-calculus property requiring arbitrarily many objects, ruling out reduction to standard finite-state model checking.
  • Run-bounded systems: For run-bounded DCDSs, µLA verification is decidable because the concrete system has a history-preserving-bisimilar finite abstraction.Verification reduces to conventional propositional µ-calculus model checking over that finite transition system.
  • Weakly acyclic systems: Run-boundedness itself is undecidable, but weak acyclicity provides an effectively checkable sufficient condition.Every weakly acyclic deterministic-service DCDS is run-bounded, and weak acyclicity can be checked in polynomial time.
  • Weakly acyclic systems: For weakly acyclic deterministic-service DCDSs, µLA verification is decidable and reduces to propositional µ-calculus model checking on a finite transition system.The condition is syntactic and guarantees run-boundedness, enabling the finite abstraction used for verification.

5. NONDETERMINISTIC SERVICES

Nondeterministic services make verification undecidable in general, but state-bounded systems admit decidability for the less expressive µLP logic. Generate-recall acyclicity provides a syntactic sufficient condition for state-boundedness and decidable verification.

  • Undecidability holds for propositional LTL safety properties over DCDSs with nondeterministic services.
  • State-bounded systems: State-boundedness permits infinitely many values across a run, provided they do not accumulate within any single state.This restriction is less limiting than run-boundedness for nondeterministic services.
  • State-bounded systems: Verification of µLA remains undecidable on state-bounded DCDSs with nondeterministic services.
  • State-bounded systems: Verification of µLP properties on state-bounded DCDSs with nondeterministic services is decidable.
  • Abstract transition systems: Algorithm RCYCL terminates on state-bounded DCDSs and constructs a finite eventually recycling pruning equivalent to the concrete transition system.The pruning can remain infinite before recycling representatives are selected, so the algorithm is needed constructively.
  • GR-acyclic DCDSs: GR-acyclic DCDSs are state-bounded, while checking state-boundedness itself is undecidable.GR+-acyclicity then yields decidable µLP verification for nondeterministic services.

6. DISCUSSION

The discussion establishes expressive equivalences between deterministic and nondeterministic service semantics while distinguishing their verification decidability properties. It also records extensions to mixed services and arbitrary first-order integrity constraints.

  • Comparison of the two semantics: Both service semantics have equivalent expressive power for unrestricted DCDSs through linear-time reductions in both directions.The reductions preserve the relevant projected transition systems.
  • Comparison of the two semantics: State-bounded nondeterministic systems cannot generally be reduced to run-bounded deterministic systems without losing the decidability distinction.The reduction from nondeterministic to deterministic services yields a non-weakly-acyclic DCDS.
  • Comparison of the two semantics: Run-bounded deterministic DCDSs inherit µLP decidability through reduction, while µLA decidability already holds directly for the deterministic case.
  • Extensions: Mixed deterministic and nondeterministic services support µLP verification when rewriting produces a GR-acyclic nondeterministic DCDS.
  • Extensions: The decidability results extend to arbitrary first-order integrity constraints under active-domain semantics by rewriting them with equality constraints.

7. RELATED WORK

The paper relates DCDS verification to artifact-centric and infinite-state-system research, while distinguishing its stronger logic and service-call semantics. Its contribution is to obtain decidability through finite abstractions or reductions under different restrictions, despite general undecidability.

  • Artifact-centric processes: Unrestricted artifact-centric and DCDS models have equivalent expressive capabilities, but differ in how they restrict processes or verification properties.The paper places its work most closely alongside verification of artifact-centric business processes.
  • Artifact-centric processes: Prior artifact-centric models generally obtain decidability only under severe restrictions, such as bounded domains or trivial pre-conditions.These works study reachability, temporal constraints, and complete executions or dead ends.
  • Artifact-centric processes with databases: Earlier database-backed approaches use first-order µ-calculus without cross-state quantification or weaker CTL variants, limiting expressibility of liveness and fairness.The cited CTL-based approach assumes bounded active domains and constructs a finite abstraction.
  • Artifact-centric processes with databases: The related database-backed work uses nulls or uninterpreted Skolem terms for externally generated values, whereas this paper interprets service calls and permits equal results from distinct calls.The difference motivates a finite abstract system that is bisimilar to an infinitely branching concrete system rather than a finite concrete system.
  • Position of the approach: The paper extends the verification setting beyond CTL and standard finite-state abstractions to expressive µ-calculus variants with cross-state object quantification.Its decidability arguments therefore require history- or persistence-aware bisimilarity, depending on the service semantics.

8. CONCLUSIONS

The conclusions summarize decidability and abstraction results for relational DCDSs and emphasize their balance between expressive verification and feasibility. They also identify finite faithful abstractions as valuable beyond merely proving decidability.

  • Conclusions: The paper’s result summary includes decidable and undecidable verification cases, while leaving verification of µL properties on bounded-run deterministic-service DCDSs open.For that open case, the paper notes that no faithful finite-state abstraction exists.
  • Conclusions: Finite faithful abstractions are presented as desirable because they offer a promising route toward practical implementation, not merely a proof of decidability.The conclusion explicitly distinguishes abstraction as an implementation-relevant goal.
  • Conclusions: DCDSs are proposed as a natural and expressive model for database-powered business processes and as a vehicle for foundational research transferable to alternative models.
  • Conclusions: The studied µL variants and corresponding DCDS classes are characterized as balancing expressivity with verification feasibility against a broader landscape of highly undecidable first-order extensions.The comparison is motivated by the existence of highly undecidable extensions even in bounded-state settings.

A.1 History Preserving Mu-Calculus

The appendix proves history-preserving invariance for µLA by first handling its non-fixpoint fragment and then extending the argument through infinitary disjunctions and fixpoint approximants.

  • Proof strategy: History-preserving invariance is proved in two stages: first for LA without predicate variables and fixpoints, then for full µLA.LA is treated as a first-order Hennessy–Milner-style logic whose semantics does not depend on second-order valuations.
  • Base invariance: The base invariance argument relates open formulas evaluated under valuations connected by a partial bijection between corresponding active-domain objects.The database isomorphism preserves answers to first-order queries under the mapped valuations.
  • Base invariance: Negation and conjunction preserve invariance by applying the induction hypothesis to the constituent formulae and their corresponding valuations.
  • Base invariance: Modal invariance follows because matching transitions have successor states related by an extended witness isomorphism, preserving the mapped valuation.The argument uses the successor-state correspondence required by history-preserving bisimulation.
  • Extension to µLA: The result extends from finite disjunctions to arbitrary countable disjunctions, after which µ-calculus fixpoints are handled through infinitary approximants.The appendix states the standard least- and greatest-fixpoint approximant relationships used for the extension.

B.2 Run-Bounded Systems

The appendix constructs a DCDS encoding of a deterministic Turing machine and uses it to establish undecidability, then relates bisimulation notions and finite abstraction results for bounded systems.

  • Undecidability construction: The undecidability proof reduces the halting problem by constructing a DCDS whose propositional safety property reflects whether a deterministic Turing machine halts.The constructed DCDS simulates machine configurations and transitions.
  • Undecidability construction: The DCDS represents the visited tape as a linear path of cell identifiers, with relations for right-neighbor links, symbols, and head position.Transition effects copy unchanged tape segments and implement entries of the machine transition relation.
  • Undecidability construction: Key constraints and transition behavior force newly generated tape cells to extend a linear path rather than create cycles or multiple predecessors.A key on the second component of right prevents reuse of an existing cell as a successor.
  • Undecidability construction: The DCDS runs correspond one-to-one with machine runs, so satisfaction of the safety property is equivalent to non-halting.The halting state sets the halted predicate used by the property.
  • Bisimulation and abstraction: For adom-inflationary systems, persistence-preserving and history-preserving bisimilarity coincide, enabling the corresponding invariance argument.The equivalence follows because every successor retains the predecessor’s active domain.
  • Bisimulation and abstraction: A run-bounded deterministic-service DCDS can be reduced to a state-bounded nondeterministic-service DCDS whose projected transition system matches the original.The construction provides a bijection between corresponding states.
  • Bisimulation and abstraction: Even a run-bounded DCDS may have infinitely many successors, and finite abstractions cannot preserve properties requiring arbitrarily many distinct successor values.The example is run-bounded by b = 3, yet every finite abstraction with k initial successors fails a property requiring k+1 distinct values.

B.3 Weakly Acyclic DCDSs

Weak acyclicity bounds the number of values that can accumulate along runs by organizing database positions according to finite ranks. This yields run-boundedness from an initially bounded active domain.

  • A Turing-machine reduction shows that deciding whether a deterministic-service DCDS is run-bounded is undecidable.
  • Weak acyclicity prevents cycles containing special edges, making every position’s maximum special-edge rank finite.
  • Values in rank-i positions are bounded inductively by a polynomial in the initial active-domain size.
  • Because the maximum rank is constant, a fixed polynomial bounds all values appearing in a run’s active domains.
  • Consequently, weak acyclicity implies data-bounded runs and therefore run-bounded deterministic DCDSs.

C.2 State-bounded Systems

State-bounded DCDSs with nondeterministic services can still support undecidable verification when formulas preserve knowledge of past objects. The proof encodes infinite data words and freeze-quantified temporal reasoning.

  • LTL with freeze quantifiers records a data value in a register and later compares subsequent values with it.
  • The reduction encodes every infinite data word as a run whose state stores one label and one data value.
  • The construction replaces register operations with existentially quantified variables whose bindings remain usable after intervening states.
  • The constructed µLA property holds exactly when the source freeze-quantified formula is unsatisfiable over infinite data words.
  • µLA verification remains undecidable even for state-bounded DCDSs with nondeterministic services.

C.3 Abstract Transition System

The paper replaces infinitely branching concrete transition systems with finite prunings that preserve the relevant behavior through isomorphism and persistence-preserving bisimilarity. State-boundedness guarantees a finite eventually recycling pruning constructible by RCYCL.

  • Infinite branching arises because fresh service results may be chosen from infinitely many values outside the current and initial active domains.
  • A pruning keeps finitely many successors while representing every equality commitment that occurs in the concrete system.
  • Every pruning is persistence-preserving bisimilar to the concrete transition system.
  • Eventually recycling prunings prevent infinitely many successive fresh-value evaluations and are therefore finite.
  • If the concrete system is state-bounded, an eventually recycling pruning exists and yields a finite-state bisimilar abstraction.
  • Algorithm RCYCL terminates on state-bounded inputs because its stored values eventually suffice to recycle subsequent service-call results.

C.4 GR-Acyclic DCDSs

GR-acyclicity enables state-boundedness analysis through an abstract dataflow transition system that tracks value propagation across normal and special edges. The resulting bounds quantify coexisting terms by graph structure.

  • Because exact state-boundedness is undecidable, the paper approximates it using a more abstract dataflow transition system.
  • The dataflow system propagates existing terms along normal edges and creates fresh terms along special edges.
  • GR-acyclicity restricts connected components to one special-edge cycle, disconnected normal-edge cycles, or a directed acyclic graph.
  • For type-A components, at most n^(d+1) · b^d · m distinct terms can coexist.
  • Type-B components obey the same n^(d+1) · b^d · m bound, while type-C components contain at most n^d · b^d · |ADOM(I0)| terms.
  • Overall, at most |ADOM(I0)| · n^(2d+1) · b^(2d) distinct terms can coexist in one concrete state.

TRAVEL REIMBURSEMENT SYSTEM

The travel reimbursement system models request submission, verification, updating, and acceptance through database actions and external service calls. Its verification examples distinguish liveness and safety properties, while the request and audit systems satisfy different acyclicity conditions.

  • Request system: The request system represents travel requests with status, employee, hotel, and flight information stored in relational data.Hotel and flight relations record dates, prices, currencies, and USD-converted amounts.
  • Request system: External services supply employee, hotel, flight, exchange-rate, and monitor-decision values during request processing.MAKEDECISION() nondeterministically returns either ‘requestConfirmed’ or ‘readyToUpdate’.
  • Request system: InitiateRequest creates a travel request and collects employee, hotel, and flight information before verification.Verification leaves travel, hotel, and flight data unchanged, while the monitor’s decision determines whether updating is required.
  • Request system: Rejected requests are updated with new hotel and flight information, reverified, and eventually accepted when the status returns to ‘readyForRequest’.The condition-action rules guard InitiateRequest, VerifyRequest, UpdateRequest, and AcceptRequest by the current status.
  • Verification and acyclicity: The request system is not GR-acyclic but is GR+-acyclic, whereas the audit system is weakly acyclic because no cycle contains a special edge.The examples also express liveness of eventual monitor decisions and safety against accepting requests with unspecified flight costs or failed audits.
Loading 1203.0024v1…