arXiv subjects

Tony Tan

Publications and source records attributed to Tony Tan.

23 records · Page 2Linked to original sources

arXiv2013

Automata for two-variable logic over trees with ordered data values

Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value from an infinite domain. They have been used as an abstraction model for reasoning tasks on {XML} and verification. However, most existing approaches consider the case where only equality test can be performed on the data values. In this paper we study data trees in which the data values come from a linearly ordered domain, and in addition to equality test, we can test whether the data value in a node is greater than the one in another node. We introduce an automata model for them which we call ordered-data tree automata (ODTA), provide its logical characterisation, and prove that its non-emptiness problem is decidable in 3-NEXPTIME. We also show that the two-variable logic on unranked trees, studied by Bojanczyk, Muscholl, Schwentick and Segoufin in 2009, corresponds precisely to a special subclass of this automata model. Then we define a slightly weaker version of ODTA, which we call weak ODTA, and provide its logical characterisation. The complexity of the non-emptiness problem drops to NP. However, a number of existing formalisms and models studied in the literature can be captured already by weak ODTA. We also show that the definition of ODTA can be easily modified, to the case where the data values come from a tree-like partially ordered domain, such as strings.

cs.LO↗

arXiv2012

Extending Büchi Automata with Constraints on Data Values

Recently data trees and data words have received considerable amount of attention in connection with XML reasoning and system verification. These are trees or words that, in addition to labels from a finite alphabet, carry data values from an infinite alphabet (data). In general it is rather hard to obtain logics for data words and trees that are sufficiently expressive, but still have reasonable complexity for the satisfiability problem. In this paper we extend and study the notion of Büchi automata for omega-words with data. We prove that the emptiness problem for such extension is decidable in elementary complexity. We then apply our result to show the decidability of two kinds of logics for omega-words with data: the two-variable fragment of first-order logic and some extensions of classical linear temporal logic for omega-words with data.

cs.LO↗

arXiv2012

Graph Reachability and Pebble Automata over Infinite Alphabets

Let D denote an infinite alphabet -- a set that consists of infinitely many symbols. A word w = a_0 b_0 a_1 b_1 ... a_n b_n of even length over D can be viewed as a directed graph G_w whose vertices are the symbols that appear in w, and the edges are (a_0,b_0),(a_1,b_1),...,(a_n,b_n). For a positive integer m, define a language R_m such that a word w = a_0 b_0 ... a_n b_n is in R_m if and only if there is a path in the graph G_w of length <= m from the vertex a_0 to the vertex b_n. We establish the following hierarchy theorem for pebble automata over infinite alphabet. For every positive integer k, (i) there exists a k-pebble automaton that accepts the language R_{2^k-1}; (ii) there is no k-pebble automaton that accepts the language R_{2^{k+1} - 2}. Based on this result, we establish a number of previously unknown relations among some classes of languages over infinite alphabets.

cs.FL↗

arXiv2011

Feasible Automata for Two-Variable Logic with Successor on Data Words

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 called weak 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 \sim, EMSO2(+1,\sim). 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 omega-strings. They can be characterized by the extension of EMSO2(+1,\sim) 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.

cs.FL↗

arXiv2009

On Pebble Automata for Data Languages with Decidable Emptiness Problem

In this paper we study a subclass of pebble automata (PA) for data languages for which the emptiness problem is decidable. Namely, we introduce the so-called top view weak PA. Roughly speaking, top view weak PA are weak PA where the equality test is performed only between the data values seen by the two most recently placed pebbles. The emptiness problem for this model is decidable. We also show that it is robust: alternating, nondeterministic and deterministic top view weak PA have the same recognition power. Moreover, this model is strong enough to accept all data languages expressible in Linear Temporal Logic with the future-time operators, augmented with one register freeze quantifier.

cs.FL↗