  Markov automata combine non-determinism, probabilistic branching, and
exponentially distributed delays. This compositional variant of continuous-time
Markov decision processes is used in reliability engineering, performance
evaluation and stochastic scheduling. Their verification so far focused on
single objectives such as (timed) reachability, and expected costs. In
practice, often the objectives are mutually dependent and the aim is to reveal
trade-offs. We present algorithms to analyze several objectives simultaneously
and approximate Pareto curves. This includes, e.g., several (timed)
reachability objectives, or various expected cost objectives. We also consider
combinations thereof, such as on-time-within-budget objectives - which policies
guarantee reaching a goal state within a deadline with at least probability $p$
while keeping the allowed average costs below a threshold? We adopt existing
approaches for classical Markov decision processes. The main challenge is to
treat policies exploiting state residence times, even for untimed objectives.
Experimental results show the feasibility and scalability of our approach.
