Exact bounds found for avoid-or-compress lengths in synchronizing automata
Exact Avoid-or-Compress Extrema for Dense Reachable Images: Defects Four and Five
Formal Languages and Automata Theory
Summary
This paper finds the exact maximum lengths needed to change images (states) in a specific kind of machine called a strongly connected synchronizing automaton, focusing on cases where the system's missing parts number four or five. The authors use mathematical constructions and computational checks to narrow down these lengths precisely, confirming the values with exhaustive analysis. They also developed new techniques to reduce the problem size, enabling them to run thorough verifications.
What this means in practice
- •For system designers: Optimize synchronization protocols by precisely understanding upper bounds on state compression in automata models.
- •For formal methods engineers: Establish correctness limits in system verification tools that model system states as synchronizing automata with known reachability constraints.
A theory result. No direct application yet.
Authors
Qichao Wang, Daoyu Dong
Abstract
Let $S$ be a reachable image of a strongly connected synchronizing automaton and $\varnothing\ne A\subsetneq S$. We determine the maximum shortest avoid-or-compress length over binary and arbitrary finite alphabets for $m=n-|S|=4$ and $m=5$. The exact values are $\min(n-|A|,11)$ and $\min(n-|A|,14)$, respectively. Uniform binary constructions attain both bounds. For the upper bounds, short-pair graphs and actual-image constraints reduce all parameters to finite necessary domains. Exhaustive checks exclude the domains, apart from a single relaxation eliminated by a multipartite overlap lemma. The largest calculation covers 3,206,988 domains.