Sciweavers

ENTCS
1998

A Testing Equivalence for Reactive Probabilistic Processes

13 years 10 months ago
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...
Marta Z. Kwiatkowska, Gethin Norman
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 1998
Where ENTCS
Authors Marta Z. Kwiatkowska, Gethin Norman
Comments (0)