Lumping-Based Equivalences in Markovian Automata and Applications to Product-Form Analyses