Modal Decomposition on Nondeterministic Probabilistic Processes.

We propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes.The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.