Automaton-based Characterisations of First Order Logic over Infinite Trees

TL;DR

This paper characterizes the expressive power of First-Order Logic over infinite trees using automata, linking it to branching-time logics and revealing its limitations to safety and co-safety properties.

Contribution

It introduces hesitant tree automata classes that exactly capture two branching-time logics, providing automata-theoretic characterizations and a normal form for o over infinite trees.

Findings

Automata classes precisely capture ext{PolPCTL} and ext{ ext{CTL}_{sf}}.

Provides a normal form for o over infinite trees in ext{ ext{PolCTL}}.

Shows o can only express safety or co-safety properties along branches.

Abstract

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.