  Probabilistic automata constitute a versatile and elegant model for
concurrent probabilistic systems. They are equipped with a compositional theory
supporting abstraction, enabled by weak probabilistic bisimulation serving as
the reference notion for summarising the effect of abstraction. This paper
considers probabilistic automata augmented with costs. It extends the notions
of weak transitions in probabilistic automata in such a way that the costs
incurred along a weak transition are captured. This gives rise to
cost-preserving and cost-bounding variations of weak probabilistic
bisimilarity, for which we establish compositionality properties with respect
to parallel composition. Furthermore, polynomial-time decision algorithms are
proposed, that can be effectively used to compute reward-bounding abstractions
of Markov decision processes in a compositional manner.

Formal Languages and Automata Theory;Logic in Computer Science