Sciweavers

FSTTCS
2010
Springer

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

13 years 7 months ago
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...
Matthew Hague, Anthony Widjaja To
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FSTTCS
Authors Matthew Hague, Anthony Widjaja To
Comments (0)