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...

• Type: Journal
• Year: 1998
• Where: ENTCS
• Authors: Marta Z. Kwiatkowska, Gethin Norman
• Keywords: ENTCS 1998, Probabilistic, Probabilistic Choice, Reactive Probabilistic Transition