Collapsible Pushdown Graphs of Level 2 are Tree-Automatic

TL;DR

This paper proves that graphs generated by level 2 collapsible pushdown systems are tree-automatic, ensuring their first-order logic theories are decidable, and extends this result to the second level of the Caucal-hierarchy.

Contribution

It establishes the tree-automaticity of level 2 collapsible pushdown graphs and their extensions, advancing the understanding of their logical and computational properties.

Findings

Graphs of level 2 collapsible pushdown systems are tree-automatic.

First-order theories of these graphs are decidable.

Extends tree-automaticity to the second level of the Caucal-hierarchy.

Abstract

We show that graphs generated by collapsible pushdown systems of level 2 are tree-automatic. Even if we allow epsilon-contractions and reachability predicates (with regular constraints) for pairs of configurations, the structures remain tree-automatic whence their first-order logic theories are decidable. As a corollary we obtain the tree-automaticity of the second level of the Caucal-hierarchy.