Reachability analysis of reversal-bounded automata on series-parallel graphs

DOI10.1007/S00236-016-0290-1MaRDI QIDQ1741900zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Rayna Dimitrova, Rupak Majumdar

Publication date 10 April 2018

Published in Acta Informatica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1509.07202

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Counter machines and verification problems.
• Reversal-Bounded Counter Machines Revisited
• scientific article; zbMATH DE number 1759429
• Reachability problem for weak multi-pushdown automata

Cites work

• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 1136090 (Why is no real title available?)
• scientific article; zbMATH DE number 1863175 (Why is no real title available?)
• scientific article; zbMATH DE number 3254905 (Why is no real title available?)
• A Temporal Graph Logic for Verification of Graph Transformation Systems
• A perfect model for bounded verification
• Automata with Reversal-Bounded Counters: A Survey
• CONCUR 2004 - Concurrency Theory
• Explicit State Model Checking for Graph Grammars
• Graph structure and monadic second-order logic. A language-theoretic approach
• Handbook of Graph Grammars and Computing by Graph Transformation
• Language, culture, computation. Computing -- theory and technology. Essays dedicated to Yaacov Choueka on the occasion of his 75th birthday, Part I
• On the Decidability Status of Reachability and Coverability in Graph Transformation Systems
• Reachability analysis of communicating pushdown systems
• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• The complexity of decision problems for finite-turn multicounter machines
• The tree width of auxiliary storage
• Tools and Algorithms for the Construction and Analysis of Systems
• Two-Way Counter Machines and Diophantine Equations

Cited in

(2)

• Reachability analysis of reversal-bounded automata on series-parallel graphs
• Reachability analysis of reversal-bounded automata on series-parallel graphs

This page was built for publication: Reachability analysis of reversal-bounded automata on series-parallel graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1741900)