Dynamic definability
Dynamic definability
复制标题
动态可定义性
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
S. Siebertz
中科院分区：
文献类型：
--
作者：
E. Grädel;S. Siebertz
我们调查了维持有关有限结构属性的知识所需的逻辑资源，该结构经历了一系列正在进行的局部变化，例如插入或将元组删除到基本关系中。我们的框架与Patnaik和Immerman的Dyn-Fo-Framework以及Dong，Libkin，Su和Wong的Foies-Foies-Foies-Foies-Foies框架密切相关，也与Weber和Schwentick的作品建立在基础上。我们假设动态过程始于任意，非空的结构，但与以前的工作相反，我们假设结构是无序的。我们展示了如何修改已知的动态算法，以进行对称可及性，两性，k边缘连接性等等，也没有顺序和动态过程从任意图开始。独立的动态系统（也称为确定性或无内存）是一个独立于更新顺序的所有辅助信息的系统。 1997年，董和SU提出了一个问题，如果存在具有对称性或两场性的历史独立动态系统，则具有fo up的独立动态系统。我们对这个问题给出了积极的答案。我们进一步表明，有一个带有FO+C-UPATES的树同构的历史独立系统。另一方面，我们表明，在无序结构上，一阶逻辑太弱，无法维护足够的信息以至于以相等的心脏查询来回答和树皮同构的动态查询。
We investigate the logical resources required to maintain knowledge about a property of a finite structure that undergoes an ongoing series of local changes such as insertion or deletion of tuples to basic relations. Our framework is closely related to the Dyn-FO-framework of Patnaik and Immerman and the FOIES-framework of Dong, Libkin, Su and Wong, and also builds on work of Weber and Schwentick. We assume that the dynamic process starts with an arbitrary, nonempty structure, but in contrast to previous work, we assume that, in general, structures are unordered. We show how to modify known dynamic algorithms for symmetric reachability, bipartiteness, k-edge connectivity and more, to work also without an order and with dynamic processes starting at an arbitrary graph. A history independent dynamic system (also called deterministic or memoryless) is one that maintains all auxiliary information independent of the update order. In 1997, Dong and Su posed the problem whether there exist history independent dynamic systems with FO-updates for symmetric reachability or bipartiteness. We give a positive answer to this question. We further show that there is a history independent system for tree isomorphism with FO+C-updates. On the other hand we show that on unordered structures first-order logic is too weak to maintain enough information to answer the equal cardinality query and the tree isomorphism query dynamically.