Abstract EXPRESS’98 to appear A Testing Equivalence for Reactive Probabilistic Processes

We consider a generalisation of Larsen and Skou’s [19] reactive probabilistic transition systems which exhibit three kinds of choice: action-guarded probabilistic choice, external (deterministic) and internal (non-deterministic) choice. We propose an operational preorder and equivalence for processes based on testing. Milner’s button pushing experiments scenario is extended with random experiments by assessing the probability of processes passing a test. Two processes are then identified with respect to the testing equivalence if they pass all tests with the same probability. The derived equivalence is a congruence for a subcalculus of CSP extended with action-guarded probabilistic choice. It is coarser than probabilistic bisimulation, yet non-probabilistic branching-time, and differs from probabilistic equivalences developed for CSP [20,22,26]. We provide a logical characterization of the equivalence in terms of the quantitative interpretation of HML of [14] and show how fixed points can be added to the logic.