An Automata Model for 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 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 emptiness problem is decidable in 3-NEXPTIME. We also show that the twovariable 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 ...

• Type: Journal
• Year: 2012
• Where: LICS
• Authors: Tony Tan
• Keywords: Automated Reasoning, Emptiness Problem, LICS 2012, Logical Characterisation, Reasoning Tasks