We gratefully acknowledge support from
the Simons Foundation
and The Alliance of Science Organisations in Germany, coordinated by TIB, MPG and HGF
Full-text links:


Current browse context:


Change to browse by:


References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Formal Languages and Automata Theory

Title: Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs

Abstract: Extensions to finite-state automata on strings, such as multi-head automata or multi-counter automata, have been successfully used to encode many infinite-state non-regular verification problems. In this paper, we consider a generalization of automata-theoretic infinite-state verification from strings to labeled series-parallel graphs. We define a model of non-deterministic, 2-way, concurrent automata working on series-parallel graphs and communicating through shared registers on the nodes of the graph. We consider the following verification problem: given a family of series-parallel graphs described by a context-free graph transformation system (GTS), and a concurrent automaton over series-parallel graphs, is some graph generated by the GTS accepted by the automaton? The general problem is undecidable already for (one-way) multi-head 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 series-parallel 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.
Comments: In Proceedings GandALF 2015, arXiv:1509.06858
Subjects: Formal Languages and Automata Theory (cs.FL)
Journal reference: EPTCS 193, 2015, pp. 100-114
DOI: 10.4204/EPTCS.193.8
Cite as: arXiv:1509.07202 [cs.FL]
  (or arXiv:1509.07202v1 [cs.FL] for this version)

Submission history

From: EPTCS [view email]
[v1] Thu, 24 Sep 2015 01:53:08 GMT (28kb)