The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Authors Matthew Hague, Anthony Widjaja To

Thumbnail PDF


  • Filesize: 458 kB
  • 12 pages

Document Identifiers

Author Details

Matthew Hague
Anthony Widjaja To

Cite AsGet BibTex

Matthew Hague and Anthony Widjaja To. The Complexity of Model Checking (Collapsible) Higher-Order 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. 228-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


We study (collapsible) higher-order pushdown systems --- theoretically robust and well-studied models of higher-order programs --- along with their natural subclass called (collapsible) higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtain tight bounds on data, expression, and combined-complexity for both (collapsible) higher-order pushdown systems and (collapsible) higher-order basic process algebra. At order-$k$, results range from polynomial to $(k+1)$-exponential time. Finally, we study (collapsible) higher-order basic process algebras as graph generators and show that they are almost as powerful as (collapsible) higher-order pushdown systems up to MSO interpretations.
  • Higher-Order
  • Collapsible
  • Pushdown Systems
  • Temporal Logics
  • Complexity
  • Model Checking


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