2016/02/24 by Flavio Ferrarotti, Klaus‐Dieter Schewe, Ferrarotti, Flavio +5 · 1 citation
Computer Science · #Advanced Database Systems and Queries #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.1602.07486
openalex publication_date 2016/02/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In database theory, the term 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ärk 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 Δ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.