Generalizing determinization from automata to coalgebras

TL;DR

This paper extends the classical powerset construction from automata to the broader setting of coalgebras, enabling a unified approach to determinization across various types of dynamical systems and equivalences.

Contribution

It introduces a generalized coalgebraic determinization framework applicable to diverse systems like Mealy machines, probabilistic automata, and pushdown automata, unifying their analysis.

Findings

Unified coalgebraic determinization method for various systems

Application to probabilistic and pushdown automata

Characterization of behavioral equivalences like failure and ready semantics

Abstract

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics.