Automata for Data Words and Data Trees

Data words and data trees appear in verification and XML processing. The term “data” means that positions of the word, or tree, are decorated with elements of an infinite set of data values, such as natural numbers or ASCII strings. This talk is a survey of the various automaton models that have been developed for data words and data trees. A data word is a word where every position carries two pieces of information: a label from a finite alphabet, and a data value from an infinite set. A data tree is defined likewise. As an example, suppose that the finite alphabet has two labels request and grant, and the data values are numbers (interpreted as process identifiers). A data word, such as the one below, can be seen as log of events that happened to the processes. request 1 request 2 request 1 request 7 request 7 request 3 grant 1 grant 3 ... The example with processes and logs can be used to illustrate how data words are used in verification. In one formulation, verificati...

• Type: Conference
• Year: 2010
• Where: RTA
• Authors: Mikolaj Bojanczyk
• Keywords: Data Tree, Data Value, Data Words, RTA 2010, Theoretical Computer Science