A Tree Logic with Graded Paths and Nominals

TL;DR

This paper introduces a decidable tree logic that extends graded modalities with deep counting along paths, including recursive navigation, addressing a gap in reasoning frameworks for path expressions with node cardinality constraints.

Contribution

It presents a novel tree logic capable of expressing deep counting along recursive paths, generalizing graded modalities, while maintaining decidability in exponential time.

Findings

The logic can express complex path-based counting constraints.

Decidability is achieved despite combining graded modalities, nominals, and inverse modalities.

The logic is suitable for reasoning in programming languages and type systems.

Abstract

Regular tree grammars and regular path expressions constitute core constructs widely used in programming languages and type systems. Nevertheless, there has been little research so far on reasoning frameworks for path expressions where node cardinality constraints occur along a path in a tree. We present a logic capable of expressing deep counting along paths which may include arbitrary recursive forward and backward navigation. The counting extensions can be seen as a generalization of graded modalities that count immediate successor nodes. While the combination of graded modalities, nominals, and inverse modalities yields undecidable logics over graphs, we show that these features can be combined in a tree logic decidable in exponential time.