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