pith. machine review for the scientific record. sign in

arxiv: 2604.26364 · v1 · submitted 2026-04-29 · 💻 cs.LO · cs.FL

Recognition: unknown

Automaton-based Characterisations of First Order Logic over Infinite Trees

Angelo Matteo, Dario Della Monica, Fabio Mogavero, Gabriele Puppis, Massimo Benerecetti

Authors on Pith no claims yet

Pith reviewed 2026-05-07 12:43 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords first-order logicinfinite treeshesitant tree automataPolPCTLCTLsfbranching-time temporal logicssafety properties
0
0 comments X

The pith

Hesitant tree automata capture first-order logic over infinite trees through two temporal logics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes automata-based characterisations for first-order logic over infinite trees. It introduces two classes of hesitant tree automata that precisely match the power of PolPCTL and CTLsf, logics previously shown to be equivalent to FO. This gives uniform automata definitions and a normal form in PolCTLs. It also reveals that FO can only express safety or co-safety properties along each branch.

Core claim

We introduce two classes of hesitant tree automata and show that they capture precisely the expressive power of 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.

What carries the argument

Two classes of hesitant tree automata that capture the expressive power of PolPCTL and CTLsf.

If this is right

  • Uniform automata-theoretic characterisations of FO over infinite trees
  • A natural normal form called PolCTLs
  • The limitation that FO expresses only safety or co-safety properties along branches

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This could enable more efficient decision procedures for FO properties on trees using automata techniques
  • Highlights differences from linear-time FO where more properties are definable
  • May lead to new normal forms or simplifications in related branching-time logics

Load-bearing premise

The prior equivalence of PolPCTL and CTLsf to first-order logic over infinite trees holds, and the hesitant automata classes are shown to match them.

What would settle it

A first-order formula over infinite trees that cannot be captured by the two classes of hesitant tree automata.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces two classes of hesitant tree automata and proves that they exactly capture the expressive power of PolPCTL and CTLsf over infinite trees. Since both logics were previously shown equivalent to FO, the automata provide uniform characterisations of FO; as a corollary the authors derive a normal form PolCTLs for CTLsf and conclude that FO can express only safety or co-safety properties along each branch.

Significance. The results supply automata-theoretic characterisations for two FO-equivalent branching-time logics and isolate a clean expressive boundary (safety/co-safety per branch). This is a useful contribution to the automata-logic interface on trees, building directly on established equivalences without introducing circularity or ad-hoc parameters.

minor comments (3)
  1. The abstract states that the trees are unordered, yet the automata definitions and acceptance conditions are not explicitly shown to be independent of any sibling ordering; a short clarifying paragraph in §3 would remove ambiguity.
  2. Notation for the two hesitant classes (e.g., HPol and Hsf) is introduced without a compact comparison table; adding such a table after the definitions would improve readability.
  3. The normal-form fragment PolCTLs is defined via a syntactic restriction on CTLsf; the manuscript should explicitly list the allowed operators and the inductive clauses for the fragment.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation of our manuscript, the recognition of its contributions in providing uniform automata-theoretic characterisations of FO via hesitant tree automata for PolPCTL and CTLsf, and the recommendation for minor revision. No major comments were raised in the report.

Circularity Check

0 steps flagged

Derivation is self-contained; no circular reductions identified

full rationale

The paper defines two new classes of hesitant tree automata and proves they exactly capture the expressive power of PolPCTL and CTLsf (previously established as equivalent to FO over infinite trees). The central results consist of independent automaton definitions followed by direct equivalence proofs to the logics, plus a derived normal form and safety/co-safety limitation as corollaries. No equation or claim reduces by construction to a fitted parameter, self-definition, or unverified self-citation chain; prior equivalences are invoked as external given facts rather than load-bearing premises that collapse the new contributions. The argument structure remains non-circular and externally grounded.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claims rest on standard definitions of FO, CTL variants, and tree automata from prior literature, plus the newly introduced hesitant classes whose correctness is asserted but not inspectable here.

axioms (2)
  • standard math Standard definitions and semantics of first-order logic, CTL, and tree automata over infinite trees
    Invoked throughout to define the logics and automata whose equivalence is claimed.
  • domain assumption Prior result that PolPCTL and CTLsf are equivalent to FO over infinite trees
    Cited as already shown; used as base for the new automata characterizations.
invented entities (2)
  • Two classes of hesitant tree automata no independent evidence
    purpose: To provide automata-theoretic characterizations of FO via PolPCTL and CTLsf
    Newly defined in the paper to capture the logics exactly.
  • PolCTLs fragment of CTL no independent evidence
    purpose: Natural normal form for FO over infinite trees
    Derived as consequence of the automata characterizations.

pith-pipeline@v0.9.0 · 5476 in / 1397 out tokens · 37324 ms · 2026-05-07T12:43:46.779207+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

18 extracted references · 17 canonical work pages

  1. [1]

    Schneider

    [AS87] Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness.Distributed computing, 2(3):117–126, 1987.path(doi: 10.1007/BF01782772). [BBMP23] M. Benerecetti, L. Bozzelli, F. Mogavero, and A. Peron. Quantifying over Trees in Monadic Second-Order Logic. InLICS’23, pages 1–13. IEEE Computer Society,

    work page doi:10.1007/bf01782772 1987

  2. [2]

    [BBMP24] M

    path(doi: 10.1109/LICS56636.2023.10175832). [BBMP24] M. Benerecetti, L. Bozzelli, F. Mogavero, and A. Peron. Automata-Theoretic Characterisations of Branching-Time Temporal Logics. InICALP’24, LIPIcs 297, pages 128:1–20. Leibniz-Zentrum fuer Informatik, 2024.path(doi: 10.4230/LIP Ics.ICALP.2024.128). [BDMM+25] Massimo Benerecetti, Dario Della Monica, Ange...

    work page doi:10.1109/lics56636.2023.10175832 2023

  3. [3]

    [BI09] M

    path(doi: 10.4204/EP T CS.428.5). [BI09] M. Boja´ nczyk and T. Idziaszek. Algebra for Infinite Forests with an Application to the Temporal logic EF. InCONCUR’09, LNCS 5710, pages 131–145. Springer,

    work page doi:10.4204/ep

  4. [4]

    Ser: Graduate Texts in Mathematics (GTM), vol

    path(doi: 10.1007/978−3−642−04081−8 10). [BIS13] M. Boja´ nczyk, T. Idziaszek, and M. Skrzypczak. Regular Languages of Thin Trees. InSTACS’13, LIPIcs 20, pages 562–573. Leibniz-Zentrum fuer Informatik,

    work page doi:10.1007/978

  5. [5]

    [BLS22] Udi Boker, Karoliina Lehtinen, and Salomon Sickert

    path(doi: 10.1007/s00224−014−9595−z). [BLS22] Udi Boker, Karoliina Lehtinen, and Salomon Sickert. On the translation of automata to lin- ear temporal logic. InInternational Conference on Foundations of Software Science and Computation Structures, pages 140–160. Springer International Publishing Cham,

    work page doi:10.1007/s00224

  6. [6]

    [Boj04] M

    path(doi: 10.48550/arXiv.2201.10267). [Boj04] M. Boja´ nczyk.Decidable Properties of Tree Languages. PhD thesis, Warsaw University, Warsaw, Poland,

    work page doi:10.48550/arxiv.2201.10267

  7. [7]

    Benedikt and L

    [BS09] M. Benedikt and L. Segoufin. Regular Tree Languages Definable in FO and in FO mod.TOCL, 11(1):1–32, 2009.path(doi: 10.1145/1614431.1614435). [BS18] U. Boker and Y. Shaulian. Automaton-Based Criteria for Membership in CTL. InLICS’18, pages 155–164. ACM, 2018.path(doi: 10.1145/3209108.3209143). [BSW12] M. Boja´ nczyk, H. Straubing, and I. Walukiewicz...

    work page doi:10.1145/1614431.1614435 2009

  8. [8]

    Carreiro

    [Car15] F. Carreiro. PDL is the Bisimulation-Invariant Fragment of Weak Chain Logic. InLICS’15, pages 341–352. IEEE Computer Society, 2015.path(doi: 10.1109/LICS.2015.40). [CMP92] E. Chang, Z. Manna, and A. Pnueli. Characterization of Temporal Prop- erty Classes. InICALP’92, LNCS 623, pages 474–486. Springer,

    work page doi:10.1109/lics.2015.40 2015

  9. [10]

    [EH85] E.A

    path(doi: 10.1145/567067.567081). [EH85] E.A. Emerson and J.Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time.JCSS, 30(1):1–24, 1985.path(doi: 10.1016/0022−0000(85)90001−7). [EJ91] E.A. Emerson and C.S. Jutla. Tree Automata, µ-Calculus, and Determinacy. InFOCS’91, pages 368–377. IEEE Computer Society, 1991.path(doi...

    work page doi:10.1145/567067.567081 1985

  10. [11]

    Esik and P

    [EW10] Z. Esik and P. Weil. Algebraic Characterization of Logically Defined Tree Languages.IJCM, 20(02):195–239, 2010.path(doi: 10.1142/S0218196710005595). [Fin72] K. Fine. In So Many Possible Worlds.NDJFL, 13:516–520,

    work page doi:10.1142/s0218196710005595 2010

  11. [12]

    Black, D.A

    [FL79] M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs.JCSS, 18(2):194–211, 1979.path(doi: 10.1016/0022−0000(79)90046−1). [Flu85] J. Flum. Characterizing Logics. InModel-Theoretic Logics, pages 77–120. Springer,

    work page doi:10.1016/0022 1979

  12. [18]

    Moller and A.M

    [MR03] F. Moller and A.M. Rabinovich. Counting on CTL*: On the Expressive Power of Monadic Path Logic. 184(1):147–159, 2003.path(doi: 10.1016/S0890−5401(03)00104−4). 38 M. BENERECETTI, D. DELLA MONICA, A. MATTEO, F. MOGAVERO, AND G. PUPPIS [MSS86] D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating Automata, the Weak Monadic The- ory of Trees and its Com...

    work page doi:10.1016/s0890 2003

  13. [20]

    [Pnu77] A. Pnueli. The Temporal Logic of Programs. InFOCS’77, pages 46–57. IEEE Computer Society, 1977.path(doi: 10.1109/SF CS.1977.32). [Pnu81] A. Pnueli. The Temporal Semantics of Concurrent Programs.TCS, 13:45–60,

    work page doi:10.1109/sf 1977

  14. [21]

    [Pot95] A

    path(doi: 10.1016/0304−3975(81)90110−9). [Pot95] A. Potthoff. First-Order Logic on Finite Trees. InTAPSOFT’95, pages 123–139. Springer,

    work page doi:10.1016/0304

  15. [22]

    [PP86] D

    path(doi: 10.1080/11663081.1992.10510780). [PP86] D. Perrin and J. Pin. First-Order Logic and Star-Free Sets.JCSS, 32(3):393–406,

    work page doi:10.1080/11663081.1992.10510780 1992

  16. [24]

    [Tho88] Wolfgang Thomas

    URL: https://lics.siglog.org/ 1987/Thomas-OnChainLogicPathLog.html. [Tho88] Wolfgang Thomas. Safety and Liveness properties in Propositional Temporal Logic: Character- izations and Decidability.Banach Center Publications, 21(1):403–417,

    1987

  17. [25]

    Vardi and P

    [VW84] M.Y. Vardi and P. Wolper. Yet Another Process Logic. InLP’83, LNCS 164, pages 501–512. Springer, 1984.path(doi: 10.1007/3−540−12896−4 383). [Wil01] Thomas Wilke. Alternating tree automata, parity games, and modal µ-calculus.Bulletin of the Belgian Mathematical Society-Simon Stevin, 8(2):359–391,

    work page doi:10.1007/3 1984

  18. [26]

    This work is licensed under the Creative Commons Attribution License

    path(doi: 10.1016/S0019−9958(83)80051−5). This work is licensed under the Creative Commons Attribution License. T o view a copy of this license, visithttps://creativecommons.org/licenses/by/4.0/or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany

    work page doi:10.1016/s0019