Abstract
We extend the classical model of multipushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gaporder 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 wellknown that the verification of any nontrivial property of multipushdown systems is undecidable, even for two stacks and for a finite datadomain. In this paper, we show the decidability of the reachability problem for the classes of data multipushdown system that admit a bounded splitwidth (or equivalently a bounded treewidth). As an immediate consequence, we obtain decidability for several subclasses of data multipushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.
BibTeX  Entry
@InProceedings{abdulla_et_al:LIPIcs:2017:7804,
author = {Parosh Aziz Abdulla and C. Aiswarya and Mohamed Faouzi Atig},
title = {{Data MultiPushdown Automata}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {38:138:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770484},
ISSN = {18688969},
year = {2017},
volume = {85},
editor = {Roland Meyer and Uwe Nestmann},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7804},
URN = {urn:nbn:de:0030drops78049},
doi = {10.4230/LIPIcs.CONCUR.2017.38},
annote = {Keywords: Pushdown Systems, ModelChecking, GapOrder, Bounded SplitWidth}
}
Keywords: 

Pushdown Systems, ModelChecking, GapOrder, Bounded SplitWidth 
Collection: 

28th International Conference on Concurrency Theory (CONCUR 2017) 
Issue Date: 

2017 
Date of publication: 

01.09.2017 