We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio~(2021) proved that two graphs satisfy the same $k$-variable and quantifier-rank-$q$ sentences if and only if they are homomorphism indistinguishable over the class 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 this graph class. This allows us to separate it from the intersection of the class of all graphs of treewidth at most $k-1$ and the class of all graphs of treedepth at most $q$, provided that $q$ is sufficiently larger than $k$. We are able to lift this separation to a (semantic) separation of the respective homomorphism indistinguishability relations. We do this by showing that the graph classes of all graphs of treedepth at most $q$ and of graphs admitting a $k$-pebble forest cover of depth $q$ are homomorphism distinguishing closed, as conjectured by Roberson~(2022). In order to prove Roberson's conjecture for the class of graphs admitting a $k$-pebble forest cover of depth $q$ we characterise the class 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 show how to transform Cop's winning strategy into a pre-tree-decomposition, which is inspired by decompositions of matroids, and then applying an intricate breadth-first `cleaning up' procedure along the pre-tree-decomposition (which may temporarily lose the property of representing a strategy), in order to achieve monotonicity while controlling the number of rounds simultaneously across all branches of the decomposition via a vertex exchange argument.

翻译：我们研究了计数量词一阶逻辑（特别是$k$变量和量词秩为$q$的片段）的表达能力，采用同态不可区分性作为工具。近期，Dawar、Jakl和Reggio（2021）证明了两个图满足相同的$k$变量和量词秩为$q$句子当且仅当它们在允许深度为$q$的$k$石子森林覆盖的图类上同态不可区分。在通过初等方法重新证明这一结果后，我们对该图类进行了图论分析。这使得我们能够将其与树宽最多为$k-1$的图类与树深最多为$q$的图类的交集区分开来，前提是$q$充分大于$k$。我们进一步将这种区分提升至相应同态不可区分性关系的（语义）分离。为此，我们证明了所有树深最多为$q$的图类与允许深度为$q$的$k$石子森林覆盖的图类在同态意义下是封闭可区分的，这验证了Roberson（2022）的猜想。为了证明允许深度为$q$的$k$石子森林覆盖的图类满足Roberson猜想，我们利用单调的警察与强盗博弈刻画了该图类。关键在于证明：若警察有获胜策略，则其也存在一个单调的获胜策略。为此，我们展示了如何将警察的获胜策略转化为一种预树分解（这一思路受拟阵分解启发），然后沿该预树分解执行一种精细的广度优先“清理”过程（该过程可能暂时丧失表示策略的性质），从而在通过顶点交换论证同时控制分解各分支轮数的条件下实现单调性。