10.4230/LIPICS.FSTTCS.2010.228
Hague, Matthew
Matthew
Hague
To, Anthony Widjaja
Anthony Widjaja
To
The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
Higher-Order
Collapsible
Pushdown Systems
Temporal Logics
Complexity
Model Checking
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
2010
2010-12-14
2010-12-14
2010-12-14
en
urn:nbn:de:0030-drops-28663
10.4230/LIPIcs.FSTTCS.2010
978-3-939897-23-1
1868-8969
10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS 2010
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
2013
8
19
228
239
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
469820 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 228-239