Testing Reactive Probabilistic Processes

TL;DR

This paper introduces a testing equivalence for reactive probabilistic processes, characterizing it via ready-traces and demonstrating its insensitivity to timing of probabilistic choices, with decidability results for finite systems.

Contribution

It defines a new testing equivalence for reactive probabilistic processes and provides a characterization and decidability results, extending existing theories.

Findings

Testing equivalence characterized by ready-traces.

Equivalence insensitive to timing of probabilistic choices.

Decidability established for finite systems.

Abstract

We define a testing equivalence in the spirit of De Nicola and Hennessy for reactive probabilistic processes, i.e. for processes where the internal nondeterminism is due to random behaviour. We characterize the testing equivalence in terms of ready-traces. From the characterization it follows that the equivalence is insensitive to the exact moment in time in which an internal probabilistic choice occurs, which is inherent from the original testing equivalence of De Nicola and Hennessy. We also show decidability of the testing equivalence for finite systems for which the complete model may not be known.