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

Date Added: Oct 2010
Format: PDF

The authors 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. They provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. They 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, they 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.