First-order model checking on generalisations of pushdown graphs.

MaRDI QIDQ3225588zbMATH OpenFDO

Authors Alexander Kartzow

Publication date 22 March 2012

Full work available at URL https://arxiv.org/abs/1202.0137

zbMATH Keywords

collapsible pushdown graphshigher-order nested pushdown treesmodel checkingRamsey quantifierstree-automatic structuresverification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nested pushdown trees are first-order interpretable in collapsible pushdown graphs of level 2. This interpretation can be extended to an interpretation of the class of higher-order nested pushdown trees in the collapsible pushdown graph hierarchy. We prove that the second level of this new hierarchy of nested trees has decidable first-order model checking. Our decidability result for collapsible pushdown graph relies on the fact that level 2 collapsible pushdown graphs are uniform tree-automatic. Our last result concerns tree-automatic structures in general. We prove that first-order logic extended by Ramsey quantifiers is decidable on all tree-automatic structures.

Recommendations

• FO Model Checking on Nested Pushdown Trees
• First-order logic on higher-order nested pushdown trees
• First-Order Logic on CPDA Graphs
• Collapsible Pushdown Graphs of Level 2 are Tree-Automatic
• Collapsible Pushdown Graphs of Level 2 are Tree-Automatic

Cited in

(9)

• On first-order logic and CPDA graphs
• Marking shortest paths on pushdown graphs does not preserve MSO decidability
• First-order model checking on nested pushdown trees is complete for doubly exponential alternating time
• First-order logic on higher-order nested pushdown trees
• Prefix rewriting for nested-words and collapsible pushdown automata
• FO Model Checking on Nested Pushdown Trees
• scientific article; zbMATH DE number 7297863 (Why is no real title available?)
• First-Order Model-Checking in Random Graphs and Complex Networks
• Tree-automatic well-founded trees

This page was built for publication: First-order model checking on generalisations of pushdown graphs.

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