First-Order Logic on Higher-Order Nested Pushdown Trees

TL;DR

This paper introduces a hierarchy of higher-order nested pushdown trees, explores their properties, and establishes the decidability of first-order model checking for the first two levels, with an algorithm for level 1.

Contribution

It generalizes nested pushdown trees to higher orders, analyzes their structure, and provides a decidability result and an algorithm for first-order model checking.

Findings

First-order model checking is decidable on the first two levels.

An EXPSPACE algorithm is developed for level 1 nested pushdown trees.

A novel pseudo-local analysis technique is introduced for Ehrenfeucht-Fraisse games.

Abstract

We introduce a new hierarchy of higher-order nested pushdown trees generalising Alur et al.'s concept of nested pushdown trees. Nested pushdown trees are useful representations of control flows in the verification of programs with recursive calls of first-order functions. Higher-order nested pushdown trees are expansions of unfoldings of graphs generated by higher-order pushdown systems. Moreover, the class of nested pushdown trees of level n is uniformly first-order interpretable in the class of collapsible pushdown graphs of level n+1. The relationship between the class of higher-order pushdown graphs and the class of collapsible higher-order pushdown graphs is not very well understood. We hope that the further study of the nested pushdown tree hierarchy leads to a better understanding of these two hierarchies. In this paper, we are concerned with the first-order model checking problem on higher-order nested pushdown trees. We show that the first-order model checking on the first two levels of this hierarchy is decidable. Moreover, we obtain an 2-EXPSPACE algorithm for the class of nested pushdown trees of level 1. The proof technique involves a pseudo-local analysis of strategies in the Ehrenfeucht-Fraisse games on two identical copies of a nested pushdown tree. Ordinary locality arguments in the spirit of Gaifman's lemma do not apply here because nested pushdown trees tend to have small diameters. We introduce the notion of relevant ancestors which provide a sufficient description of the FO_k -type of each element in a higher-order nested pushdown tree. The local analysis of these ancestors allows us to prove the existence of restricted winning strategies in the Ehrenfeucht-Fraisse game. These strategies are then used to create a first-order model checking algorithm.