2026-10-03T06:15:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2866 2024-03-06T09:33:38Z ddc:004 open_access

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems Hague, Matthew To, Anthony Widjaja Higher-Order Collapsible Pushdown Systems Temporal Logics Complexity Model Checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthew Hague and Anthony Widjaja To 2010 Is Part Of LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2010.228 urn:nbn:de:0030-drops-28663 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.228 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode