动态数据库驱动系统的近期有界验证（扩展版）
Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version)
摘要：
我们提出了一个形式主义模型数据库驱动的系统，称为数据库操作系统（DMS）。DMS的操作通过向数据库中添加新元素、从关系中删除元组以及向关系中添加元组来修改关系数据库的当前实例。由动作修改的元素由（完整的）一阶查询选择。DMS是一个高度表达的模型，可以被认为是一个简洁的表示一个无限状态的关系转换系统，在文献中提出的类似的模型。我们提出了一元二阶逻辑（MSO-FO）的原因出现沿运行的数据库实例的序列。不出所料，DMS对MSO-FO的线性时间模型检验问题是不可判定的。针对可判定性，提出了DMS的欠近似模型检验，其中欠近似参数为“新近界”。在$k$ -最近-有界运行中，只有当前活动域中最近的$k$元素可以被操作修改。可以通过增加新近度的界限来验证更多的运行。我们的主要结果表明，最近有界的模型检验的DMS对MSO-FO是可判定的，通过减少的可满足性问题的MSO嵌套的话。
英文摘要：
We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. DMS is a highly expressive model and can be thought of as a succinct representation of an infinite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of DMS against MSO-FO is undecidable. Towards decidability, we propose under-approximate model checking of DMS, where the under-approximation parameter is the "bound on recency". In a $k$-recency-bounded run, only the most recent $k$ elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of DMS against MSO-FO is decidable, by a reduction to the satisfiability problem of MSO over nested words.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
