Counting Branches in Trees Using Games
Arnaud Carayol, Axel Haddad, Olivier Serre

TL;DR
This paper investigates finite automata on infinite binary trees with relaxed acceptance criteria based on the number of rejecting or accepting branches, introducing game-based methods to analyze their $ ext{omega}$-regular languages.
Contribution
It introduces a game-based framework for automata with cardinality constraints on branches, proving their languages are always $ ext{omega}$-regular and providing new proofs for existing results.
Findings
Acceptance games characterize automata with branch cardinality constraints.
Languages accepted under these criteria are always $ ext{omega}$-regular.
New proofs for classical results on accepting branches in automata.
Abstract
We study finite automata running over infinite binary trees. A run of such an automaton is usually said to be accepting if all its branches are accepting. In this article, we relax the notion of accepting run by allowing a certain quantity of rejecting branches. More precisely we study the following criteria for a run to be accepting: - it contains at most finitely (resp countably) many rejecting branches; - it contains infinitely (resp uncountably) many accepting branches; - the set of accepting branches is topologically "big". In all situations we provide a simple acceptance game that later permits to prove that the languages accepted by automata with cardinality constraints are always -regular. In the case (ii) where one counts accepting branches it leads to new proofs (without appealing to logic) of an old result of Beauquier and Niwinski.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Computability, Logic, AI Algorithms · Formal Methods in Verification
