Profile Trees for B\"uchi Word Automata, with Application to Determinization
Seth Fogarty (Trinity University), Orna Kupferman (Hebrew University, of Jerusalem), Moshe Y. Vardi (Rice University), Thomas Wilke, (Christian-Albrechts-Universit\"at zu Kiel)

TL;DR
This paper introduces a new theoretical framework using profile trees for determinizing Büchi automata, providing a more declarative and conceptually clear approach compared to previous operational methods.
Contribution
It extends profile theory to Büchi automata, establishing a finite-branch profile tree structure and proposing a novel, declarative determinization construction.
Findings
Profile trees contain finitely many infinite branches.
The new determinization method is more declarative than existing ones.
Theoretical grounding improves understanding and implementation.
Abstract
The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi…
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.
