What is the conjecture
The Černý conjecture is a central open problem in automata theory concerning the length of synchronizing words in deterministic finite automata.
A deterministic finite automaton (DFA) is a triple $A = (Q, \Sigma, \delta)$, where:
-
$Q$ is a finite set of states,
-
$\Sigma$ is a finite input alphabet,
-
$\delta : Q \times \Sigma \to Q$ is the transition function.
A word $w \in \Sigma^*$ is called a synchronizing word if there exists a state $q_0 \in Q$ such that
$$\delta(q, w) = q_0 \quad \text{for all } q \in Q.$$ In other words, reading the word $w$ sends every state of the automaton to the same single state.
The automaton is called synchronizing if such a word exists.
The Černý conjecture asserts that if a synchronizing DFA has $n$ states, then it admits a synchronizing word of length at most $(n - 1)^2$.
This bound is known to be tight: there exists a family of automata (the Černý automata) achieving this bound.
Source: https://en.wikipedia.org/wiki/Černý_conjecture, https://en.wikipedia.org/wiki/Synchronizing_word
Prerequisites needed
Building blocks (from Mathlib):
- Deterministic finite automata (DFA)
Missing pieces (not in current Mathlib):
- Synchronization theory (reset words, synchronizing automata)
AMS categories
- ams-68 (Computer Science — Automata Theory and Formal Languages)
- ams-05 (Combinatorics)
What is the conjecture
The Černý conjecture is a central open problem in automata theory concerning the length of synchronizing words in deterministic finite automata.
A deterministic finite automaton (DFA) is a triple$A = (Q, \Sigma, \delta)$ , where:
A word$w \in \Sigma^*$ is called a synchronizing word if there exists a state $q_0 \in Q$ such that
$$\delta(q, w) = q_0 \quad \text{for all } q \in Q.$$ In other words, reading the word $w$ sends every state of the automaton to the same single state.
The automaton is called synchronizing if such a word exists.
The Černý conjecture asserts that if a synchronizing DFA has$n$ states, then it admits a synchronizing word of length at most $(n - 1)^2$ .
This bound is known to be tight: there exists a family of automata (the Černý automata) achieving this bound.
Source: https://en.wikipedia.org/wiki/Černý_conjecture, https://en.wikipedia.org/wiki/Synchronizing_word
Prerequisites needed
Building blocks (from Mathlib):
Missing pieces (not in current Mathlib):
AMS categories