FO Model Checking on Nested Pushdown Trees

DOI10.1007/978-3-642-03816-7_39MaRDI QIDQ3182946zbMATH OpenOpenAlexFDO

Authors Alexander Kartzow

Publication date 16 October 2009

Published in Mathematical Foundations of Computer Science 2009 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03816-7_39

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• First-order model checking on generalisations of pushdown graphs.
• First-order logic on higher-order nested pushdown trees
• First-order model checking on nested pushdown trees is complete for doubly exponential alternating time
• Languages of Nested Trees
• First-Order Logic on CPDA Graphs

Cites work

• Alternation
• Collapsible pushdown automata and recursion schemes
• Languages of Nested Trees
• On the structure of graphs in the Caucal hierarchy

Cited in

(5)

• First-order model checking on nested pushdown trees is complete for doubly exponential alternating time
• First-order logic on higher-order nested pushdown trees
• First-order model checking on generalisations of pushdown graphs.
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Languages of Nested Trees

This page was built for publication: FO Model Checking on Nested Pushdown Trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3182946)