Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

How Concise are Chains of co-Büchi Automata?

Rüdiger Ehlers

Abstract

Chains of co-Büchi 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üchi 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üchi 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.

How Concise are Chains of co-Büchi Automata?

Abstract

Chains of co-Büchi 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üchi 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üchi 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.
Paper Structure (11 sections, 15 theorems, 7 equations, 6 figures)

This paper contains 11 sections, 15 theorems, 7 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A short introduction to chains of co-Büchi automata
  4. An example COCOA
  5. Some additional definitions and notes in the context of COCOA
  6. On the conciseness of COCOA
  7. DPW conciseness over COCOA
  8. LTL $\rightarrow$ COCOA
  9. COCOA disjunction/conjunction can cause an exponential blow-up
  10. Complementing COCOA
  11. Conclusion

Key Result

Proposition 4.1

Let $\inf$ be the function mapping a sequence to the set of elements occurring infinitely often in the sequence. For every $k \in \mathbb{N}$, the language $L^k = \{w \in \{1, \ldots, k\}^\omega \mid \min(\inf(w)) \text{ is even}\}$ can be represented by a deterministic parity automaton with a singl

Figures (6)

  • Figure 1: An example COCOA
  • Figure 2: A deterministic co-Büchi automaton (parametrized for some $k \in \mathbb{N}$ and $1 \leq j \leq n$) for the co-Büchi languages used in the proof of Theorem \ref{['thm:conciseNessWithSingleSuffixLanguage']}
  • Figure 3: A minimal DPW for $\mathcal{L}(\mathcal{C}^2)$ with a marking of how the states map to combinations of states in a COCOA for the same language. Transitions with a color of $1$ are drawn as dotted.
  • Figure 4: A deterministic co-Büchi automaton for the language $L^k_i$. Rejecting transitions are dashed.
  • Figure 5: Overview of how the sets $\{ L^k_i \cap \hat{L}^k_j\}_{0 \leq i \leq k, 0 \leq j \leq k}$ (for $k=4$) compose $C^k_0, \ldots, C_{2k}^k$ in Theorem \ref{['thm:conjunctionBecomesBig']}
  • ...and 1 more figures

Theorems & Definitions (39)

  • Definition 3.1: DBLP:conf/fsttcs/EhlersS22, Def. 1
  • Proposition 4.1: Appears to not have been stated previously elsewhere
  • proof
  • Proposition 4.2: Already appearing in abbreviated form in DBLP:journals/corr/abs-2410-01021 based on remarks in DBLP:conf/tacas/EhlersK24
  • proof
  • Theorem 4.3
  • Definition 4.4
  • Lemma 4.5
  • proof
  • Lemma 4.6
  • ...and 29 more