Bisimulation through probabilistic testing (Q1175940)

A test language and a notion of probabilistic testability of concurrent process properties are presented. Properties expressed as formulas within Hennessy-Milner logic are testable and as a consequence non-bisimilar processes can be distinguished through testing. A new process relation called \({2\over3}\)-bisimulation is introduced. The relation lies strictly between that of simulation and bisimulation. For probabilistic transition systems for which there is a limit to the probability of transitions it is proved that two processes are \({2\over3}\)-bisimilar iff they satisfy the same limited modal logic formulas. Probabilistic modal logic is introduced and it is shown that the induced notion of probabilistic bisimilarity characterizes the limit as to the distinguishing power of the test language. The probabilistic bisimulation is strictly stronger than bisimulation.