Fibrational Perspectives on Determinization of Finite-State Automata

Colcombet and Petris an argued that automata may be usefully considered from a functorial perspective, introducing a general notion of "V -automaton" based on functors into V .This enables them to recover different standard notions of automata by choosing V appropriately, and they further analyzed the determinization for Rel-automata using the Kleisli adjunction between Set and Rel.In this paper, we revisit Colcombet and Petris an's analysis from a fibrational perspective, building on Mellis and Zeilberger's recent alternative but related definition of categorical automata as functors p : Q C satisfying the finitary fiber and unique lifting of factorizations property.In doing so, we improve the understanding of determinization in three regards: Firstly, we carefully describe the universal property of determinization in terms of forward-backward simulations.Secondly, we generalize the determinization procedure for Rel automata using a local adjunction between Span(Set) and Rel, which provides us with a canonical forward simulation.Finally we also propose an alternative determinization based on the multiset relative adjunction which retains paths, and we leverage this to provide a canonical forward-backward simulation.