Feasible Automata for Two-Variable Logic with Successor on Data Words
Feasible Automata for Two-Variable Logic with Successor on Data Words
复制标题
DOI：
10.1007/978-3-642-28332-1_30
复制
发表时间：
2011-10
影响因子：
--
通讯作者：
A. Kara;T. Schwentick;Tony Tan
中科院分区：
文献类型：
--
作者：
A. Kara;T. Schwentick;Tony Tan
我们介绍了一个自动机模型的数据字，这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是（语义）的数据自动机，介绍了Bojanczyk，等的限制。在2006年，我们称之为弱数据自动机。它的表达能力比数据自动机差，而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+ 1且数据值相等的存在一元二阶逻辑EMSO 2（+ 1，~）完全对应。它遵循从以前的工作，大卫，等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外，我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2（+ 1，~）的扩张来刻画，扩张中存在量词对无限集合的作用.最后，通过对弱数据自动机的非空性问题进行非确定性多项式时间约简，得到了其非空性问题的复杂性界。
We introduce an automata model for data words, that is words that carry at each position a symbol from a finite alphabet and a value from an unbounded data domain. The model is (semantically) a restriction of data automata, introduced by Bojanczyk, et. al. in 2006, therefore it is calledweak data automata. It is strictly less expressive than data automata and the expressive power is incomparable with register automata. The expressive power of weak data automata corresponds exactly to existential monadic second order logic with successor + 1 and data value equality ~, EMSO2( + 1,~). It follows from previous work, David, et. al. in 2010, that the nonemptiness problem for weak data automata can be decided in 2-NEXPTIME. Furthermore, we study weak Büchi automata on dataω-strings. They can be characterized by the extension of EMSO2( + 1,~) with existential quantifiers for infinite sets. Finally, the same complexity bound for its nonemptiness problem is established by a nondeterministic polynomial time reduction to the nonemptiness problem of weak data automata.