We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment $\mathsf{C}^k_q$, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio (2021) proved that two graphs satisfy the same $\mathsf{C}^k_q$-sentences iff they are homomorphism indistinguishable over the class $\mathcal{T}^k_q$ of graphs admitting a $k$-pebble forest cover of depth $q$. After reproving this result using elementary means, we provide a graph-theoretic analysis of $\mathcal{T}^k_q$. This allows us to separate $\mathcal{T}^k_q$ from the intersection $\mathcal{TW}_{k-1} \cap \mathcal{TD}_q$, provided that $q$ is sufficiently larger than $k$. Here $\mathcal{TW}_{k-1}$ is the class of all graphs of treewidth at most $k-1$ and $\mathcal{TD}_q$ is the class of all graphs of treedepth at most $q$. We are able to lift this separation to a separation of the respective homomorphism indistinguishability relations $\equiv_{\mathcal{T}^k_q}$ and $\equiv_{\mathcal{TW}_{k-1} \cap \mathcal{TD}_q}$. We do this by showing that the classes $\mathcal{TD}_q$ and $\mathcal{T}^k_q$ are homomorphism distinguishing closed, as conjectured by Roberson (2022). In order to prove Roberson's conjecture for $\mathcal{T}^k_q$, we characterise $\mathcal{T}^k_q$ in terms of a monotone Cops-and-Robber game. The crux is to prove that if Cop has a winning strategy then Cop also has a winning strategy that is monotone. To that end, we transform Cops' winning strategy into a pree-tree-decomposition, which is inspired by decompositions of matroids, and then apply an intricate breadth-first cleaning up procedure along the pree-tree-decomposition (which may temporarily lose the property of representing a strategy). Thereby, we achieve monotonicity while controlling the number of rounds across all branches of the decomposition via a vertex exchange argument.

翻译：我们利用同态不可区分性研究带计数量词的一阶逻辑的表达能力，特别是$k$-变量且量词秩为$q$的片段$\mathsf{C}^k_q$。近期，Dawar、Jakl与Reggio（2021）证明：两个图满足相同的$\mathsf{C}^k_q$-句子当且仅当它们在深度为$q$的$k$-卵石森林覆盖图类$\mathcal{T}^k_q$上同态不可区分。在采用初等方法重新证明此结果后，我们对$\mathcal{T}^k_q$进行了图论分析。这使得我们能够分离$\mathcal{T}^k_q$与交集类$\mathcal{TW}_{k-1} \cap \mathcal{TD}_q$，前提是$q$足够大于$k$。这里$\mathcal{TW}_{k-1}$表示树宽至多为$k-1$的所有图类，而$\mathcal{TD}_q$表示树深至多为$q$的所有图类。我们进一步将这一分离提升至相应同态不可区分关系$\equiv_{\mathcal{T}^k_q}$与$\equiv_{\mathcal{TW}_{k-1} \cap \mathcal{TD}_q}$的分离。为此，我们证明$\mathcal{TD}_q$和$\mathcal{T}^k_q$是同态区分闭类，这证实了Roberson（2022）的猜想。为证明关于$\mathcal{T}^k_q$的Roberson猜想，我们通过单调的警察与强盗博弈刻画$\mathcal{T}^k_q$。关键难点在于证明：若警察存在获胜策略，则警察亦存在单调的获胜策略。为此，我们将警察的获胜策略转化为受拟阵分解启发的预树分解，再沿该预树分解执行精细的广度优先清理过程（该过程可能暂时丧失策略表征性质）。通过顶点交换论证，我们最终在控制分解所有分支上的回合数的同时实现了单调性。