Extensions to finitestate automata on strings, such as multihead automata or multicounter automata, have been successfully used to encode many infinitestate nonregular verification problems. In this paper, we consider a generalization of automatatheoretic infinitestate verification from strings to labeled seriesparallel graphs. We define a model of nondeterministic, 2way, concurrent automata working on seriesparallel graphs and communicating through shared registers on the nodes of the graph. We consider the following verification problem: given a family of seriesparallel graphs described by a contextfree graph transformation system (GTS), and a concurrent automaton over seriesparallel graphs, is some graph generated by the GTS accepted by the automaton? The general problem is undecidable already for (oneway) multihead automata over strings. We show that a bounded version, where the automata make a fixed number of reversals along the graph and use a fixed number of shared registers is decidable, even though there is no bound on the sizes of seriesparallel graphs generated by the GTS. Our decidability result is based on establishing that the number of context switches is bounded and on an encoding of the computation of bounded concurrent automata to reduce the emptiness problem to the emptiness problem for pushdown automata.
