Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width

La Torre, Salvatore; Parlato, Gennaro

doi:10.4230/LIPIcs.FSTTCS.2012.173

Document

Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width

Authors Salvatore La Torre, Gennaro Parlato

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2012-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2012.173.pdf

Filesize: 0.61 MB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2012.173
URN: urn:nbn:de:0030-drops-38563

Subject Classification

Keywords

Model-checking
multi-threaded programs
sequentialization
tree-width

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

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.

Cite As Get BibTex

Salvatore La Torre and Gennaro Parlato. Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 173-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.FSTTCS.2012.173

Author Details

Salvatore La Torre

Gennaro Parlato

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail