SOS-based modal decomposition on nondeterministic probabilistic processes