|Ph.D Student||Tan Tony|
|Subject||Pebble Automata for Data Languages: Separation,|
Decidability and Undecidability
|Department||Department of Computer Science||Supervisor||Professor Michael Kaminski|
|Full Thesis text|
In this thesis we continue the study of pebble automata for data languages, which were first introduced by Neven, Schwentick and Vianu in 2001. In essence, pebble automata (PA) are finite state automata with a finite number of pebbles. The pebbles are placed on the input word in the stack discipline: first in--last out, to mark positions in the input word. One pebble can only mark one position and the last pebble placed serves as the automaton head. The automaton moves from one state to another depending on the label of the position and the equality tests among data values marked by the pebbles. As established by Neven, Schwentick and Vianu, PA languages have desirable closure properties; but undesirable in terms of application: their emptiness problem in general is undecidable.
We present the boundary of the subclass of PA for which the emptiness problem is decidable. We call this subclass top view weak PA. We show this subclass inherits most of the desirable qualities of PA such as robustness: equivalence among alternating, nondeterministic and deterministic versions; and logical closure properties. It is also strong enough to contain the languages defined by Linear Temporal Logic augmented by one register freeze quantifier.
We also establish a number of separation results. In particular, we establish the hierarchy of PA languages based on the number of pebbles and separation of Monadic Second Order logic from PA languages. In addition, we also show that PA is a robust model of computation for data languages. Some of our results settle questions left open by Neven, Schwentick and Vianu.