Compositionality for Markov Reward Chains with Fast Transitions
J. Markovski, A. Sokolova, N. Trcka and E.P. de Vink

A parallel composition is defined for Markov reward chains with
stochastic discontinuity, and with fast and silent transitions. In
this setting, compositionality with respect to the relevant
aggregation preorders is established. For Markov reward chains with
fast transitions the preorders are tau-lumping and
tau-reduction. Discontinuous Markov reward chains are limits of Markov
reward chains with fast transitions, and have related notions of
lumping and reduction. Markov reward chains with silent transitions
are equivalence classes of Markov reward chains with fast transitions
and come equipped with the lifted preorders tau-sim-lumping and
tau-sim-reduction. In total, six compositionality results are
presented. Additionally, the parallel operators involved are related
by a continuity result.