Document Open Access Logo

Saturation of Concurrent Collapsible Pushdown Systems

Author Matthew Hague

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2013.313.pdf
  • Filesize: 0.66 MB
  • 13 pages

Document Identifiers

Subject Classification

Keywords
  • Concurrency
  • Automata
  • Higher-Order
  • Verification
  • Model-Checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls.  While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability.  To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability
problems for multi-stack collapsible pushdown systems have been little studied. Here, we study ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques, showing decidability of control state reachability and giving a regular representation of all configurations that can reach a given control state.

Cite As Get BibTex

Matthew Hague. Saturation of Concurrent Collapsible Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 313-325, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.FSTTCS.2013.313

Author Details

Matthew Hague
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact