How Concise are Chains of co-B\"uchi Automata?

TL;DR

This paper investigates the conciseness of chains of co-Büchi automata (COCOA), revealing their potential for exponential size reduction over deterministic parity automata and demonstrating that Boolean operations can cause exponential growth in automaton size.

Contribution

It provides the first analysis of COCOA conciseness, showing exponential advantages over deterministic parity automata and highlighting limitations in size preservation under Boolean operations.

Findings

COCOA can be exponentially more concise than deterministic parity automata.

Boolean operations on COCOA can cause exponential size blow-up.

Disjunction and conjunction of certain languages require exponential automaton size increase.

Abstract

Chains of co-B\"uchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary omega-regular languages. They can be minimized in polynomial time and are hence an attractive language representation for applications in which normally, deterministic omega-automata are used. While it is known how to build COCOA from deterministic parity automata, little is currently known about their relationship to automaton models introduced earlier than COCOA. In this paper, we analyze the conciseness of chains of co-B\"uchi automata. We provide three main results and give an overview of the implications of these results. First of all, we show that even in the case that all automata in the chain are deterministic, chains of co-B\"uchi automata can be exponentially more concise than deterministic parity automata. We then present two main results that together negatively answer the question if this conciseness is retained when performing Boolean operations (such as disjunction, conjunction, and complementation) over COCOA. For the binary operations, we show that there exist families of languages for which their application leads to an exponential growth of the sizes of the automata. The families have the property that when representing them using deterministic parity automata, taking the disjunction or conjunction of the family elements only requires a polynomial blow-up. We finally show that an exponential blow-up is also unavoidable when complementing a COCOA, as this operation can require redistributing with which colors words need to be recognized.