First-Order Logic on Higher-Order Nested Pushdown Trees

Details First-Order Logic on Higher-Order Nested Pushdown Trees First-Order Logic on Higher-Order Nested Pushdown Trees

2012-02-09

arxiv.org/abs/1202.1980v1

Computer Science

Logic in Computer Science

41 pages

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

First-Order Logic on Higher-Order Nested Pushdown Trees does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with First-Order Logic on Higher-Order Nested Pushdown Trees, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and First-Order Logic on Higher-Order Nested Pushdown Trees will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-157223