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

We study (collapsible) higher-order pushdown systems -- theoretically robust and well-studied models of higher-order programs -- along with their natural subclass called (collapsible) higherorder 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. 1998 ACM Subject Classification D.2.4 Keywords and phrases Higher-Order, Collapsible, Pushdown Systems, Temporal Logics, Complexity, Model Checking Digital Object Identifier 10.4230/LIPIcs.FSTT...

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Matthew Hague, Anthony Widjaja To
• Keywords: Basic Process Algebra, FSTTCS 2010, Linear-time Temporal Logics, Software Engineering, Temporal Logics