Complementation of Emerson-Lei Automata (Technical Report)

TL;DR

A specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition.

Abstract

We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it combines a given complementation algorithm for a condition $\varphi$ in a way that the resulting procedure handles conditions of the form Fin ${} \land \varphi$. The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes.

Figures (2)

• Figure 1: $\mathcal{A}_{\mathit{ex}}$
• Figure 2: A labelled run DAG of $\mathcal{A}_{\mathit{ex}}$ over the word $caa(cab)^\omega \notin \mathcal{L}(\mathcal{A}_{\mathit{ex}})$