Min-Plus Weighted Finite Automata (WFAs) are a quantitative extension of Boolean automata whereby each word is assigned an integer, instead of being accepted or rejected.
Applications of WFAs fall on a wide spectrum including verification, rewriting systems, tropical algebra, speech and image processing and have been key to proving the star-height conjecture.
Unlike Boolean automata, WFAs cannot always be determinized. The decidability of whether a WFA admits an equivalent deterministic WFA is a long standing open problem.
We prove that this problem is decidable.
As part of the proof, we develop a new toolbox for reasoning about the run structure of weighted automata.