Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

History-Deterministic Büchi Automata are Succinct

Antonio Casares, Aditya Prakash, K. S. Thejaswini

TL;DR

A history-deterministic Buchi automaton that has strictly less states than every language-equivalent deterministic Buchi automaton is described, and proving its succinctness requires the combination of theoretical insights and the aid of computers.

Abstract

We describe a history-deterministic Büchi automaton that has strictly less states than every language-equivalent deterministic Büchi automaton. This solves a problem that had been open since the introduction of history-determinism and actively investigated for over a decade. Our example automaton has 65 states, and proving its succinctness requires the combination of theoretical insights together with the aid of computers.

History-Deterministic Büchi Automata are Succinct

TL;DR

A history-deterministic Buchi automaton that has strictly less states than every language-equivalent deterministic Buchi automaton is described, and proving its succinctness requires the combination of theoretical insights and the aid of computers.

Abstract

We describe a history-deterministic Büchi automaton that has strictly less states than every language-equivalent deterministic Büchi automaton. This solves a problem that had been open since the introduction of history-determinism and actively investigated for over a decade. Our example automaton has 65 states, and proving its succinctness requires the combination of theoretical insights together with the aid of computers.
Paper Structure (16 sections, 4 theorems, 4 equations, 4 figures)

This paper contains 16 sections, 4 theorems, 4 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Organisation.
  3. Preliminaries
  4. Automata and history-determinism
  5. Automata.
  6. History-determinism.
  7. Structure of HD Büchi automata
  8. Simulation relation.
  9. Reach-covering.
  10. Semantic determinism.
  11. Normal form.
  12. Simplified Büchi automata.
  13. Graveyard of conjectures and the automata that killed them
  14. A motivating example.
  15. The Rewiring Conjectures
  16. ...and 1 more sections

Key Result

Theorem 2

There is a history/̄deterministic Büchi automaton that has strictly fewer states than every language/̄equivalent deterministic Büchi automaton.

Figures (4)

  • Figure 1: A HD Büchi automaton ${\mathcal{A}_{\mathtt{BKKS}}}$ that is not determinisable by pruning. States labelled $I$ are identified as the same state. Double green arrows represent significant transitions.
  • Figure 2: A Büchi automaton that is not HD.
  • Figure 3: Two language-equivalent deterministic Büchi automata to the automaton from Figure \ref{['fig:BKKS13']}.
  • Figure 4: HD Büchi automaton ${\mathcal{A}_{\mathtt{strong}}}$ for which the strong-rewiring conjecture is false. To improve readability, we represent the automaton "by chunks"; note that some states appear multiple times (in total, the automaton has $17$ states).

Theorems & Definitions (8)

  • Example 1
  • Theorem 2
  • Example 3
  • Lemma 4: Pra25
  • Conjecture 5: Weak-rewiring conjecture
  • Conjecture 6: Strong-rewiring conjecture
  • Lemma 7
  • Lemma 8