Support for expected rate rewards in Markov automata model checking

Markov automata model checking in the ModelChecking project is currently only implemented for unbounded reachability and expected transition reward properties.

Task: Implement support for unbounded expected rate reward properties. I first thought this can be done symbolically (i.e. on the automata network level), but due to guards and maximal progress disabling Markovian transitions, it may rather need to be integrated into state space exploration.