A Complete Logic for Database Abstract State Machines

TL;DR

This paper introduces a formal logic for Database Abstract State Machines (DB-ASMs), enabling rigorous reasoning about non-deterministic database transformations with a sound and complete proof system.

Contribution

It extends existing ASM logic to handle non-determinism in database transformations, formalizing update sets and related features within a new logical framework.

Findings

Developed a sound and complete proof system for DB-ASM logic.

Formalized non-determinism and update sets in the logic.

Provided a verification tool for properties of database transformations.

Abstract

In database theory, the term $\textit{database transformation}$ was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and St\"ark for ASMs. In particular, we develop a rigorous proof system for the logic for DB-ASMs, which is proven to be sound and complete. The most difficult challenge to be handled by the extension is a proper formalisation capturing non-determinism of database transformations and all its related features such as consistency, update sets or multisets associated with DB-ASM rules. As the database part of a state of database transformations is a finite structure and DB-ASMs are restricted by allowing quantifiers only over the database part of a state, we resolve this problem by taking update sets explicitly into the logic, i.e. by using an additional modal operator $[X]$, where $X$ is interpreted as an update set $\Delta$ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.