Oxford logo
[KN98b] M. Kwiatkowska and G. Norman. A Testing Equivalence for Reactive Probabilistic Processes . In A Testing Equivalence for Reactive Probabilistic Processes , volume 16(2) of Electronic Notes in Theoretical Computer Science, pages 114-132, Elsevier Science. September 1998. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (112 KB)  pdf pdf (284 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. We consider a generalisation of Larsen and Skou's 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. We provide a logical characterization of the equivalence in terms of the quantitative interpretation of HML and show how fixed points can be added to the logic.