2026-08-12T07:16:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7804 2024-03-06T10:41:10Z ddc:004 open_access

Data Multi-Pushdown Automata Abdulla, Parosh Aziz Aiswarya, C. Atig, Mohamed Faouzi Pushdown Systems Model-Checking Gap-Order Bounded Split-Width 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Parosh Aziz Abdulla and C. Aiswarya and Mohamed Faouzi Atig 2017 Is Part Of LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2017.38 urn:nbn:de:0030-drops-78049 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.38 eng https://creativecommons.org/licenses/by/3.0/legalcode