If multiple symbols behave the same on all transitions, it is possible to "quotient" the symbols and work with simpler automata, in particular allowing for lower storage and smaller Cartesian products.
Depending on how much you want to save, this can be tricky, as even storage of the equivalences can lead to blowup. (Essentially, you're allowed at most one "sparse" or one "dense" equivalence relation.)
Additionally, dealing with things like quantifier elimination is tricky.
But here is an example case where this can be extremely useful:
Evaluating "x1 = 0 & x2 = 0 & ... " leads to an exponentially large alphabet with precisely one nontrivial path.
This means that the trivial paths behave the same on all transitions.
If implemented properly, this case could be done in effectively linear storage and processing.
If multiple symbols behave the same on all transitions, it is possible to "quotient" the symbols and work with simpler automata, in particular allowing for lower storage and smaller Cartesian products.
Depending on how much you want to save, this can be tricky, as even storage of the equivalences can lead to blowup. (Essentially, you're allowed at most one "sparse" or one "dense" equivalence relation.)
Additionally, dealing with things like quantifier elimination is tricky.
But here is an example case where this can be extremely useful:
Evaluating "x1 = 0 & x2 = 0 & ... " leads to an exponentially large alphabet with precisely one nontrivial path.
This means that the trivial paths behave the same on all transitions.
If implemented properly, this case could be done in effectively linear storage and processing.