Finite Variable Counting Logics with Restricted Requantification

TL;DR

This paper investigates the expressive power and algorithmic implications of restricted requantification in finite variable counting logics, introducing new tools like pebble games and Weisfeiler-Leman variants to analyze their properties.

Contribution

It introduces a novel framework for studying counting logics with limited requantification, including new pebble games and Weisfeiler-Leman algorithms, and clarifies their expressive and algorithmic capabilities.

Findings

Restricted requantification affects graph identification complexity.

Non-requantifiable variables add only polynomial space complexity.

Graphs with bounded tree-depth are identifiable with few requantifiable variables.

Abstract

Counting logics with a bounded number of variables form one of the central concepts in descriptive complexity theory. Although they restrict the number of variables that a formula can contain, the variables can be nested within scopes of quantified occurrences of themselves. In other words, the variables can be requantified. We study the fragments obtained from counting logics by restricting requantification for some but not necessarily all the variables. Similar to the logics without limitation on requantification, we develop tools to investigate the restricted variants. Specifically, we introduce a bijective pebble game in which certain pebbles can only be placed once and for all, and a corresponding two-parametric family of Weisfeiler-Leman algorithms. We show close correspondences between the three concepts. By using a suitable cops-and-robber game and adaptations of the Cai-F\"urer-Immerman construction, we completely clarify the relative expressive power of the new logics. We show that the restriction of requantification has beneficial algorithmic implications in terms of graph identification. Indeed, we argue that with regard to space complexity, non-requantifiable variables only incur an additive polynomial factor when testing for equivalence. In contrast, for all we know, requantifiable variables incur a multiplicative linear factor. Finally, we observe that graphs of bounded tree-depth and 3-connected planar graphs can be identified using no, respectively, only a very limited number of requantifiable variables.