We study the expressive power of First-Order Logic (\FO) over (unordered) infinite trees, with the aim of identifying robust characterisations in terms of branching-time specification formalisms. While such correspondences are well understood in the linear-time setting, the branching-time case presents well-known structural challenges. To this end, we introduce two classes of hesitant tree automata and show that they capture precisely the expressive power of two branching-time temporal logics, namely \PolPCTL and \CTLsf, both of which have been previously shown to be equivalent to \FO over infinite trees. These results provide uniform automata-theoretic characterisations and yield a natural normal form for the latter in terms of a new fragment of \CTLs called \PolCTLs. As a consequence, we identify a fundamental limitation of \FO in this setting: along each branch, it can express only properties that are either safety or co-safety, thereby revealing a sharp expressive boundary for first-order definability over infinite trees.

翻译：我们研究（无序）无限树上一阶逻辑（\FO）的表达能力，旨在通过分支时间规范形式化体系识别其鲁棒性特征。尽管此类对应关系在线性时间背景下已得到充分理解，但分支时间情形存在众所周知的结构性挑战。为此，我们引入两类犹豫树自动机，并证明它们恰好捕获两种分支时间时态逻辑（即\PolPCTL和\CTLsf）的表达能力——此前已有研究表明二者均等价于无限树上的\FO。这些结果提供了统一的自动机理论特征刻画，并由此为后者导出一个基于\CTLs新片段（称为\PolCTLs）的自然范式。作为推论，我们识别出\FO在该设定中的根本局限性：沿每条分支，它仅能表达安全性或共安全性属性，从而揭示了无限树上一阶可定义性的尖锐表达边界。