Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/41794
Title: Reachability analysis of reversal-bounded automata on series-parallel graphs
Authors: Dimitrova, Rayna
Majumdar, Rupak
First Published: 18-Nov-2016
Publisher: Springer Verlag
Citation: Acta Informatica, 2016, 55 (2), pp. 153-189
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 automatatheoretic infinite-state verification from strings to labelled 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 can be bounded and on an encoding of the computation of bounded concurrent automata that allows us to reduce the reachability problem to the emptiness problem for pushdown automata.
DOI Link: 10.1007/s00236-016-0290-1
ISSN: 0001-5903
eISSN: 1432-0525
Links: https://link.springer.com/article/10.1007%2Fs00236-016-0290-1
http://hdl.handle.net/2381/41794
Version: Publisher Version
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © the authors, 2016 This is an open-access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
10.1007%2Fs00236-016-0290-1.pdfPublished (publisher PDF)708.64 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.