Global Model Checking of Ordered Multi-Pushdown Systems

Author Mohamed Faouzi Atig

Thumbnail PDF


  • Filesize: 418 kB
  • 12 pages

Document Identifiers

Author Details

Mohamed Faouzi Atig

Cite AsGet BibTex

Mohamed Faouzi Atig. Global Model Checking of Ordered Multi-Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 216-227, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


In this paper, we address the verification problem of ordered multi-pushdown systems: A multi-stack extension of pushdown systems that comes with a constraint on stack operations such that a pop can only be performed on the first non-empty stack. First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given $w$-regular property (expressible in linear-time temporal logics or the linear-time $\mu$-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of $w$-regular properties for ordered multi-pushdown systems (matching its lower-bound).
  • Concurrent Programs
  • Pushdown Systems
  • Global Model-Checking


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
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