Abstract :
We study the graph reachability problem as a language over an infinite alphabet. Namely, we view a word of even length a0b0 ... an b_n over an infinite alphabet as a directed graph with the symbols that appear in a0b0 ... anbn as the vertices and (a0, b0),...,(an, bn) as the edges. We prove that for any positive integer k, k pebbles are sufficient for recognizing the existence of a path of length 2k - 1 from the vertex a0 to the vertex bn, but are not sufficient for recognizing the existence of a path of length 2k+1 - 2 from the vertex a0 to the vertex bn. Based on this result, we establish a number of relations among some classes of languages over infinite alphabets.
Keywords :
automata theory; directed graphs; formal logic; number theory; reachability analysis; directed graph reachability problem; first-order logic; infinite alphabet; path recognition; pebble automata; positive integer; Automata; Automatic testing; Computer science; Formal verification; Informatics; Logic; Natural languages; Petri nets; XML; Graph reachability; infinite alphabets; pebble automata;
