On Determinizability of Tropical Weighted Automata

We survey the history of the determinizability problem for min-plus (tropical) weighted automata.

Traditional automata accept or reject their input, and are therefore Boolean, in the sense that their language is a function L : Σ ^* → {0, 1}. They are well-understood, and have provided the theoretical basis for many applications, most notably in formal verification. However, today's rich systems and properties are often unsuitable to model with Boolean models, mostly due to the presence of quantitative elements, such as energy, probability, counters, etc.