DFA Resolutions of B¨uchi Automata:Pro-Objects, Closure Properties, and Model Checking

We develop a categorical framework in which B¨uchi automata are representedas pro-objects (formal cofiltered limits) in the category AutΣ of deterministic fi-nite automata over an alphabet Σ. The key ingredient is a family of endofunctorsBn: AutΣ →AutΣ, each of which counts the number of times a run passes throughthe accepting state, together with natural transformations πn: Bn+1 →Bn that as-semble into an inverse system. We call this inverse system the DFA resolution ofthe B¨uchi automaton.Within this framework, intersection of B¨uchi-recognisable languages correspondsto the categorical product of their resolutions—computed levelwise in AutΣ—indirect analogy with derived tensor products in homological algebra, where the cor-rect construction is performed on projective resolutions rather than on the objectsthemselves. We show that closure under union and intersection follow as formalconsequences of the pro-object structure. We also provide a pro-object formulationof the emptiness problem and discuss its connection to model checking. Finally,we outline extensions to nondeterministic B¨uchi automata and other acceptanceconditions