18.12.2025
Polynomial-time minimizable automata for omega-regular languages
Abstract
For languages over finite words, automata types that permit polynomial-time minimization are well-known. For languages over infinite words, as used when specifying the behavior of reactive systems, finding an automaton class that has a polynomial-time minimization algorithm proved to be substantially more difficult. While some such representations for so-called lasso languages exists, their use in applications is limited and tends to be restricted to language learning.
In this talk, we present recent progress towards solving this problem. We start by showing how arbitrary omega-regular languages can be canonically decomposed into a series of co-Büchi languages, each of which can in turn be made canonical and minimized by representing them as history-deterministic co-Büchi automata with transition-based acceptance. We show how to translate such a chain of co-Büchi automata (COCOA) representation into a fixpoint formula for performing reactive synthesis over a game graph.
Afterwards, we consider the question if the main ideas of the COCOA representation can be lifted to an automaton model in which the language to be represented is only encoded as a single automaton, as usual in automata theory. We show that a reinterpretation of how history-deterministic co-Büchi automata accept words can be combined with parity acceptance to obtain a polynomial-time minimizable automaton model for arbitrary omega-regular languages. Finally, we show that this new automaton model is useful both for reactive synthesis and probabilistic verification.
Bio
Rüdiger Ehlers received his doctorate from Saarland University in 2012 and held researcher positions at UC Berkeley and Cornell University before becoming a junior research group leader at the University of Bremen. Since 2019, he is professor for embedded systems at Clausthal University of Technology.
Photo provided by speaker
For languages over finite words, automata types that permit polynomial-time minimization are well-known. For languages over infinite words, as used when specifying the behavior of reactive systems, finding an automaton class that has a polynomial-time minimization algorithm proved to be substantially more difficult. While some such representations for so-called lasso languages exists, their use in applications is limited and tends to be restricted to language learning.
In this talk, we present recent progress towards solving this problem. We start by showing how arbitrary omega-regular languages can be canonically decomposed into a series of co-Büchi languages, each of which can in turn be made canonical and minimized by representing them as history-deterministic co-Büchi automata with transition-based acceptance. We show how to translate such a chain of co-Büchi automata (COCOA) representation into a fixpoint formula for performing reactive synthesis over a game graph.
Afterwards, we consider the question if the main ideas of the COCOA representation can be lifted to an automaton model in which the language to be represented is only encoded as a single automaton, as usual in automata theory. We show that a reinterpretation of how history-deterministic co-Büchi automata accept words can be combined with parity acceptance to obtain a polynomial-time minimizable automaton model for arbitrary omega-regular languages. Finally, we show that this new automaton model is useful both for reactive synthesis and probabilistic verification.
Bio
Rüdiger Ehlers received his doctorate from Saarland University in 2012 and held researcher positions at UC Berkeley and Cornell University before becoming a junior research group leader at the University of Bremen. Since 2019, he is professor for embedded systems at Clausthal University of Technology.
Photo provided by speaker