Implementation relations and probabilistic schedulers in the distributed test architecture

- New (probabilistic) type of scheduler.
- Three new implementation relations for distributed testing of PIOTSs.
- Analysis with respect to relations with deterministic schedulers.
- The strongest relations are equivalent.
- The weakest relations differ.

We present a complete framework to formally test systems with distributed ports where some choices are probabilistically quantified while other choices are non-deterministic. We define different implementation relations, that is, relations that state what it means for a system to be a valid implementation of a specification. We also study how these relate. In order to define these implementation relations we use probabilistic schedulers, a more powerful version, including probabilistic choices, of a notion of scheduler introduced in our previous work. Probabilistic schedulers, when applied to either a specification or an implementation, resolve all the possible non-determinism, so that we can compare purely probabilistic systems.