2026-07-20T12:09:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3856 2024-03-06T10:34:32Z ddc:004 open_access

Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width La Torre, Salvatore Parlato, Gennaro Model-checking multi-threaded programs sequentialization tree-width We present a novel fixed-point algorithm to solve reachability of multi-stack pushdown systems restricted to runs where matching push and pop transitions happen within a bounded number of context switches. The followed approach is compositional, in the sense that the runs of the system are summarized by bounded-size interfaces. Moreover, it is suitable for a direct implementation and can be exploited to prove two new results. We give a sequentialization for this class of systems, i.e., for each such multi-stack pushdown system we construct an equivalent single-stack pushdown system that faithfully simulates the behavior of each thread. We prove that the behavior graphs (multiply nested words) for these systems have bounded tree-width, and thus a number of decidability results can be derived from Courcelle's theorem. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Salvatore La Torre and Gennaro Parlato 2012 Is Part Of LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2012.173 urn:nbn:de:0030-drops-38563 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.173 eng https://creativecommons.org/licenses/by/3.0/legalcode