数据库操作进程的抽象域
Abstract Domains for Database Manipulating Processes
AI总结：
本文基于抽象解释原理提出数据库操作系统（DMS）的进程语义框架，通过抽象域统一语义等价的数据库集合，并研究抽象在互模拟等价下的语义保持性，以支持完整DMS的自动推理。
摘要：
数据库操作系统（DMS）形式化了关系数据库上的操作，例如添加新元组或删除现有元组。为确保足以刻画实际数据库系统的表达能力，DMS操作引入了守护表达式，即基于可数值域的一阶公式。这些特性带来了无限状态、无限分支的进程，从而使诸如状态可达性等性质的自动推理变得不可处理。因此，最近的大多数方法都限制DMS以获得可判定的片段。然而，一个既能刻画完整DMS，又能纳入有效的数据抽象和进程等价概念的全面语义框架仍是一个未解决的问题。在本文中，我们基于抽象解释原理提出了DMS进程语义。具体域由所有有效数据库组成，而抽象域采用不同的构造来统一那些在DMS守护语言的特定片段下语义等价的数据库集合。抽象域与具体域之间的联系通过同态映射有效建立，其性质和限制取决于所考虑的DMS片段的表达能力。我们为规范的DMS片段实例化了该框架，并研究了抽象在互模拟等价意义下的语义保持性，互模拟是操作进程语义中最强的等价概念之一。
英文摘要：
Database manipulating systems (DMS) formalize operations on relational databases like adding new tuples or deleting existing ones. To ensure sufficient expressiveness for capturing practical database systems, DMS operations incorporate guarding expressions first-order formulas over countable value domains. Those features impose infinite state, infinitely branching processes thus making automated reasoning about properties like the reachability of states intractable. Most recent approaches, therefore, restrict DMS to obtain decidable fragments. Nevertheless, a comprehensive semantic framework capturing full DMS, yet incorporating effective notions of data abstraction and process equivalence is an open issue. In this paper, we propose DMS process semantics based on principles of abstract interpretation. The concrete domain consists of all valid databases, whereas the abstract domain employs different constructions for unifying sets of databases being semantically equivalent up to particular fragments of the DMS guard language. The connection between abstract and concrete domains is effectively established by homomorphic mappings whose properties and restrictions depend on the expressiveness of the DMS fragment under consideration. We instantiate our framework for canonical DMS fragments and investigate semantical preservation of abstractions up to bisimilarity, being one of the strongest equivalence notions for operational process semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
