uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Data Multi-Pushdown Automata
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Chennai Mathematical Institute .
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2017 (English)In: The 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany / [ed] Roland Meyer and Uwe Nestmann, Dagstuhl, Germany, 2017, Vol. 85, 38:1-38:17 p.Conference paper, Published paper (Refereed)
Abstract [en]

We extend the classical model of multi-pushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gap-order constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number. It is well-known that the verification of any non-trivial property of multi-pushdown systems is undecidable, even for two stacks and for a finite data-domain. In this paper, we show the decidability of the reachability problem for the classes of data multi-pushdown system that admit a bounded split-width (or equivalently a bounded tree-width). As an immediate consequence, we obtain decidability for several subclasses of data multi-pushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.

Place, publisher, year, edition, pages
Dagstuhl, Germany, 2017. Vol. 85, 38:1-38:17 p.
Series
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 85
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-337127DOI: 10.4230/LIPIcs.CONCUR.2017.38ISBN: 978-3-95977-048-4 (print)OAI: oai:DiVA.org:uu-337127DiVA: diva2:1168329
Conference
The 28th International Conference on Concurrency Theory, CONCUR 2017
Projects
UPMARC
Available from: 2017-12-20 Created: 2017-12-20 Last updated: 2018-01-13

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Aziz Abdulla, ParoshAtig, Mohamed Faouzi
By organisation
Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 24 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf