Marco Bernardo

Davide Sangiorgi

Valeria Vignudelli

On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems

Testing equivalences have been deeply investigated on fully nondeterministic processes, as well as on processes featuring probabilities and internal nondeterminism. This is not the case with reactive probabilistic processes, for which it is only known that the discriminating power of probabilistic bisimilarity is achieved when admitting a copying capability within tests. In this paper, we introduce for reactive probabilistic processes three testing equivalences without copying, which are respectively based on reactive probabilistic tests, fully nondeterministic tests, and nondeterministic and probabilistic tests. We show that the three testing equivalences are strictly finer than probabilistic failuretrace equivalence, and that the one based on nondeterministic and probabilistic tests is strictly finer than the other two, which are incomparable with each other. Moreover, we provide a number of facts that lead us to conjecture that (i) may testing and must testing coincide on reactive probabilistic processes and (ii) nondeterministic and probabilistic tests reach the same discriminating power as probabilistic bisimilarity.

Introduction

Many relations have been defined in concurrency theory to capture the notion of "same behavior". They range from branching-time relations like (bi)simulations, which are very sensitive to branching points, to linear-time relations based on (decorated) traces, which in contrast abstract to different extents from those points. Most of these relations can be characterized in terms of testing scenarios. Two processes are testing equivalent if, when interacting with them by means of tests encompassing a success predicate, they result in the observation of the same outcomes. By varying the power of tests, it is possible to recover different behavioral relations in the linear-time/branching-time spectrum [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF].

The formalization of testing equivalence that we consider in this paper was first introduced in [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF], and then revisited in [START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF]. It is very general, in the sense that it is defined on processes featuring both internal nondeterminism and probabilities. We will describe such processes through a nondeterministic and probabilistic extension of labeled transition systems (LTS) [START_REF] Keller | Formal verification of parallel programs[END_REF], which we call NPLTS, where the target of each transition is a probability distribution over the set of states -in the style of [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF][START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF] -rather than a single state.

The idea at the basis of this probabilistic testing equivalence, which we denote by ∼ PTe-⊔⊓ , is as follows. The interaction system, resulting from an NPLTS process under test and an NPLTS observer, does not have a unique probability of succeeding, but several success probabilities, one for each maximal resolution of nondeterminism. Only the supremum (⊔) and the infimum (⊓) of these success probabilities are taken into account in [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF], so that two processes are deemed equivalent if they result, for each possible test, in the same suprema and infima. Following the terminology of classical testing equivalence [START_REF] De Nicola | Testing equivalences for processes[END_REF], the constraint on suprema (resp. infima) -yielding ∼ PTe-⊔ (resp. ∼ PTe-⊓ ) -represents the may (resp. must) part; we know from [START_REF] Deng | Remarks on testing probabilistic processes[END_REF] that ∼ PTe-⊓ is strictly finer than ∼ PTe-⊔ in the absence of divergence, i.e., infinite computations whose steps are all invisible.

The relation ∼ PTe-⊔⊓ of [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF] coincides, over processes and tests resulting in interaction systems with finitely many maximal resolutions, with a slightly finer variant comparing success probabilities of individual maximal resolutions, for which several characterizations were given. In [START_REF] Segala | Testing probabilistic automata[END_REF], it was shown that ∼ PTe-⊔ coincides with the coarsest congruence contained in the probabilistic tracedistribution equivalence of [START_REF] Segala | A compositional trace-based semantics for probabilistic automata[END_REF] and ∼ PTe-⊓ coincides with the coarsest congruence contained in a probabilistic failure-distribution equivalence. 1 Besides providing logical and equational characterizations, in [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF] it was later shown that ∼ PTe-⊔ coincides with a probabilistic simulation equivalence akin to that of [START_REF] Lynch | Compositionality for probabilistic automata[END_REF] and ∼ PTe-⊓ coincides with a novel probabilistic failure-simulation equivalence. Such characterizations of ∼ PTe-⊔⊓ , together with its position in the spectrum of NPLTS behavioral equivalences studied in [START_REF] Bernardo | Relating strong behavioral equivalences for processes with nondeterminism and probabilities[END_REF], reveals that this equivalence has a higher discriminating power with respect to the fully nondeterministic case.

When both the processes and the tests are fully nondeterministic, i.e., LTS models, ∼ PTe-⊔⊓ boils down to the classical testing equivalence of [START_REF] De Nicola | Testing equivalences for processes[END_REF]. In this case, as shown in [START_REF] Nicola | Extensional equivalences for transition systems[END_REF] ∼ PTe-⊔ coincides with trace equivalence and, in the absence of divergence, ∼ PTe-⊓ coincides with failure equivalence [START_REF] Brookes | A theory of communicating sequential processes[END_REF]. Several subsequent works addressed how to make classical testing equivalence more powerful. In [START_REF] Phillips | Refusal testing[END_REF], a higher discriminating power -the one of failure-trace equivalence [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF] -was reached by equipping tests with the possibility of expressing the refusal of performing certain actions (refusal testing). Then, it was illustrated in [START_REF] Abramsky | Observational equivalence as a testing equivalence[END_REF] that the discriminating power of bisimulation equivalence [START_REF] Milner | Communication and Concurrency[END_REF] can be achieved if, in addition to refusals, two further ingredients are introduced: making copies of intermediate states of the processes under test (copying capability) and enumerating all computations at some point inside a test and combining the related information (global testing). As later observed in [START_REF] Jonsson | Testing and refinement for nondeterministic and probabilistic processes[END_REF][START_REF] Deng | Remarks on testing probabilistic processes[END_REF][START_REF] Bernardo | Revisiting trace and testing equivalences for nondeterministic and probabilistic processes[END_REF], an alternative way of enhancing the discriminating power of classical testing equivalence consists of including probabilities within tests.

Unlike the NPLTS case and the LTS case, very little is known about the discriminating power of the relation ∼ PTe-⊔⊓ of [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF] over NPLTS models not admitting internal nondeterminism, i.e., Markov decision processes (MDP) [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF] or, equivalently, reactive probabilistic labeled transition systems (RPLTS) [START_REF] Van Glabbeek | Reactive, generative and stratified models of probabilistic processes[END_REF].

An analogous relation was investigated only in [START_REF] Kwiatkowska | A testing equivalence for reactive probabilistic processes[END_REF] for possibly replicated deterministic tests applied to RPLTS models extended with a form of internal choice; this relation is strictly coarser than the probabilistic bisimilarity of [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF].

A testing approach for RPLTS models not concerned with extremal success probabilities was studied in [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF][START_REF] Van Breugel | Domain theory, testing and simulation for labelled Markov processes[END_REF]. It is based on tests formalized through a nonprobabilistic testing language, which allows a tuple of tests to be performed independently on as many copies of the current state of the process under test. The copying capability turns out to be sufficient for the resulting testing equivalence to coincide with the probabilistic bisimilarity of [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], as two RPLTS models that are not probabilistic bisimilar can be distinguished by some such test with probability arbitrarily close to one. As noticed in [START_REF] Bloom | A remark on bisimulation between probabilistic processes[END_REF], this statistical approach cannot be exploited for classical bisimilarity, because there are bisimilar LTS models for which no pair of computable probabilizations in the form of RPLTS models renders them indistinguishable with respect to the considered tests.

The purpose of this paper is to examine the discriminating power of the relation ∼ PTe-⊔⊓ of [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF] when the processes under test are RPLTS models. On the observer side, we consider three different classes of tests: RPLTS, LTS, and NPLTS. In all the three cases, ∼ PTe-⊔⊓ will turn out to be strictly finer than a probabilistic extension of failure-trace equivalence, thereby confirming the power of the interplay between probabilities and nondeterminism discussed in [START_REF] Jonsson | Testing and refinement for nondeterministic and probabilistic processes[END_REF][START_REF] Deng | Remarks on testing probabilistic processes[END_REF][START_REF] Bernardo | Revisiting trace and testing equivalences for nondeterministic and probabilistic processes[END_REF] even when testing RPLTS processes. We then show that the discriminating power of LTS tests and the discriminating power of RPLTS tests are not only below the discriminating power of NPLTS tests, but also incomparable with each other.

Finally, in the setting of testing RPLTS processes, we bring up two problems whose solution seems far from being trivial. The first one refers to may testing and must testing; while the latter is known to be strictly finer than the former for divergence-free LTS or NPLTS processes, we conjecture that they coincide in the case of RPLTS processes. The second one refers to the discriminating power of ∼ PTe-⊔⊓ under NPLTS tests; although no copying capability is admitted, we conjecture that the same identification power as the probabilistic bisimilarity of [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] is achieved. Our conjectures will be substantiated by a number of facts. Some preliminary results for RPLTS testing are contained in [START_REF] Bernardo | On the discriminating power of passivation and higher-order interaction[END_REF]. However, that paper focusses on higher-order languages and addresses, for RPLTS processes, only the case of LTS-based tests generated by CCS-like calculi [START_REF] Milner | Communication and Concurrency[END_REF] with and without refusal. In contrast, here we systematically investigate the discriminating power of testing equivalence ∼ PTe-⊔⊓ when applied to RPLTS processes under each of the three classes of tests: RPLTS, LTS, and NPLTS.

This paper is organized as follows. In Sect. 2, we introduce the various LTSlike models that will be used throughout the paper. In Sect. 3, we present the spectrum of behavioral equivalences for RPLTS models by extending results over fully probabilistic processes proved in [START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF][START_REF] Huynh | On some equivalence relations for probabilistic processes[END_REF]. In Sect. 4, we define the three variants of ∼ PTe-⊔⊓ . In Sect. 5, we place the three variants in the RPLTS spectrum and relate their respective discriminating powers. Finally, in Sect. 6 we discuss the two open problems mentioned above and motivate our conjectures about their solution.

Background

In this section, we provide definitions and notations for the various LTS-like models used in the paper to formalize processes, tests, and interaction systems.

Nondeterministic and Probabilistic Processes

The most expressive model that we need is the one that will be used to represent interaction systems, as well as the most powerful observers that we consider. Since it may contain both internal nondeterminism and probabilities, we start by defining it as a slight variation of simple probabilistic automata [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF]. In the next two subsections, we derive the submodels employed to represent processes under test, as well as less powerful observers. Definition 1. A nondeterministic and probabilistic labeled transition system, NPLTS for short, is a triple (S, A, -→) where S is an at most countable set of states, A is a countable set of transition-labeling actions, and -→ ⊆ S × A × Distr (S) is a transition relation, with Distr (S) being the set of discrete probability distributions over S.

A transition (s, a, ∆) is written s a -→ ∆. State s ′ ∈ S is not reachable from s via that a-transition if ∆(s ′ ) = 0,
otherwise it is reachable with probability p = ∆(s ′ ). The reachable states form the support of ∆, i.e., supp(∆) = {s ′ ∈ S | ∆(s ′ ) > 0}. The choice among all the outgoing transitions of s is nondeterministic and can be influenced by the external environment, while the choice of the target state for a specific transition is probabilistic and made internally.

In this setting, a computation is a sequence of state-to-state steps, each denoted by s a -→ s ′ and derived from a state-to-distribution transition s a -→ ∆. Definition 2. Let L = (S, A, -→) be an NPLTS and s, s ′ ∈ S. A sequence c:

s 0 a1 -→ s 1 a2 -→ s 2 . . . s n-1 an -→ s n is a computation of L of length n from s = s 0 to s ′ = s n iff for all i = 1, . . . , n there exists a transition s i-1 ai -→ ∆ i such that s i ∈ supp(∆ i ), with ∆ i (s i ) be- ing the execution probability of step s i-1 ai -→ s i conditioned on the selection of transition s i-1 ai -→ ∆ i of L at state s i-1 .
Computation c is maximal iff it is not a proper prefix of any other computation. We denote by C fin (s) the set of finite-length computations from s.

A resolution of a state s of an NPLTS L is the result of a possible way of resolving nondeterminism starting from s. A resolution is a tree-like structure, whose branching points are probabilistic choices corresponding to target distributions of transitions. This is obtained by unfolding from s the graph structure of L and by selecting at each reached state at most one of its outgoing transitions. Definition 3. Let L = (S, A, -→ L ) be an NPLTS and s ∈ S. An NPLTS Z = (Z, A, -→ Z ) is a resolution of s iff there exists a state correspondence function corr Z : Z → S such that s = corr Z (z s ) for some z s ∈ Z, and for all z ∈ Z it holds that:

-If z a -→ Z ∆, then corr Z (z) a -→ L ∆ ′ with corr Z being injective over supp(∆) and ∆(z ′ ) = ∆ ′ (corr Z (z ′ )) for all z ′ ∈ supp(∆). -If z a1 -→ Z ∆ 1 and z a2 -→ Z ∆ 2 , then a 1 = a 2 and ∆ 1 = ∆ 2 .
Resolution Z is maximal iff, for all z ∈ Z, whenever z has no outgoing transitions, then corr Z (z) has no outgoing transitions either. We respectively denote by Res(s) and Res max (s) the sets of resolutions and maximal resolutions of s.

Since Z ∈ Res(s) is fully probabilistic in that each of its states has at most one outgoing transition, the probability prob(c) of executing c ∈ C fin (z s ) can be computed as the product of the (no longer conditional) execution probabilities of the individual steps of c. This notion is lifted to C ⊆ C fin (z s ) by letting prob(C) = c∈C prob(c) whenever none of the computations in C is a proper prefix of one of the others.

Reactive Probabilistic Processes

A reactive probabilistic process can be described as an RPLTS. This is an NPLTS (S, A, -→) in which, for all s ∈ S and a ∈ A, whenever s

a -→ ∆ 1 and s a -→ ∆ 2 , then ∆ 1 = ∆ 2 .
This means that internal nondeterminism is not admitted. Given a state s ∈ S and a trace α ∈ A * , if no resolution of s contains computations labeled with α, then the probability of executing α from s is 0. Otherwise, due to the absence of internal nondeterminism, there exists a resolution of s containing the set C(s, α) of all the computations from s labeled with α, in which case the probability of executing α from s is assumed to be the value prob(C(s, α)) computed in any of these resolutions containing C(s, α).

Fully Nondeterministic Processes

The behavior of a fully nondeterministic process is usually represented through an LTS, which can be viewed as an NPLTS (S, A, -→) in which every transition leads to a Dirac distribution, i.e., a distribution that concentrates all the probability mass into a single target state. Formally, a Dirac transition s a -→ δ s ′ fulfills δ s ′ (s ′ ) = 1 and δ s ′ (s ′′ ) = 0 for all s ′′ ∈ S \ {s ′ }. In these processes without probabilities, resolutions reduce to computations.

The Spectrum of Equivalences for RPLTS Processes

We know from [START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF][START_REF] Huynh | On some equivalence relations for probabilistic processes[END_REF][START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] that the linear-time/branching-time spectrum of behavioral equivalences for fully probabilistic processes is narrower than the one for fully nondeterministic processes [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF] as in the former many equivalences coincide. This is the case also with reactive probabilistic processes, as we now show.

Let L = (S, A, -→) be an RPLTS and s, s 1 , s 2 ∈ S. We introduce probabilistic trace-based equivalences on L as follows by analogy with [START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF][START_REF] Huynh | On some equivalence relations for probabilistic processes[END_REF]:

-C(s, α) is the set of computations from s labeled with trace α ∈ A * . s 1 ∼ PTr s 2 iff prob(C(s 1 , α)) = prob(C(s 2 , α)) for all α ∈ A * . -CC(s, α) is the set of completed computations from s labeled with α ∈ A * .
s 1 ∼ PCTr s 2 iff s 1 ∼ PTr s 2 and prob(CC(s 1 , α)) = prob(CC(s 2 , α)) for all α ∈ A * . -FC(s, ϕ), where ϕ = (α, F ) is a failure pair, is the set of computations from s labeled with α such that the last state of each computation cannot perform any action in F .

s 1 ∼ PF s 2 iff prob(FC(s 1 , ϕ)) = prob(FC(s 2 , ϕ)) for all ϕ ∈ A * × 2 A . -RC(s, ̺)
, where ̺ = (α, R) is a ready pair, is the set of computations from s labeled with α such that the set of actions that can be performed by the last state of each computation is precisely R.

s 1 ∼ PR s 2 iff prob(RC(s 1 , ̺)) = prob(RC(s 2 , ̺)) for all ̺ ∈ A * × 2 A . -FT C(s, φ), where φ = (a 1 , F 1 ) . . . (a n , F n ) is a failure trace,
F i . s 1 ∼ PFTr s 2 iff prob(FT C(s 1 , φ)) = prob(FT C(s 2 , φ)) for all φ ∈ (A × 2 A ) * . -RT C(s, ρ), where ρ = (a 1 , R 1 ) . . . (a n , R n ) is
a ready trace, is the set of computations from s labeled with a 1 . . . a n such that the set of actions that can be performed by the state reached by each computation after the i-th

step, 1 ≤ i ≤ n, is precisely R i . s 1 ∼ PRTr s 2 iff prob(RT C(s 1 , ρ)) = prob(RT C(s 2 , ρ)) for all ρ ∈ (A × 2 A ) * .
Probabilistic bisimilarity ∼ PB for RPLTS processes was defined in [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], while probabilistic similarity ∼ PS can be introduced as follows by analogy with [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]. Given a binary relation R over S, its lifting R d to Distr (S) is defined by letting (∆ 1 , ∆ 2 ) ∈ R d iff there exists a function w : S × S → R [0,1] such that:

-w(s 1 , s 2 ) > 0 =⇒ (s 1 , s 2 ) ∈ R for all s 1 , s 2 ∈ S; -∆ 1 (s 1 ) = s ′ ∈S w(s 1 , s ′ ) for all s 1 ∈ S; -∆ 2 (s 2 ) = s ′ ∈S w(s ′ , s 2 ) for all s 2 ∈ S. A binary relation R on S is a probabilistic simulation iff, whenever (s 1 , s 2 ) ∈ R, then for all a ∈ A it holds that s 1 a -→ ∆ 1 implies s 2 a -→ ∆ 2 with (∆ 1 , ∆ 2 ) ∈ R d ;
the equivalence ∼ PS is the kernel of the largest probabilistic simulation. Relation R is a probabilistic bisimulation iff it is a symmetric probabilistic simulation; the equivalence ∼ PB is the largest probabilistic bisimulation.

It was shown in [START_REF] Baier | Domain equations for probabilistic processes[END_REF] that ∼ PB and ∼ PS coincide, hence the variants in between (ready similarity, failure similarity, completed similarity) collapse too. Moreover, the proofs of the results in [START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF][START_REF] Huynh | On some equivalence relations for probabilistic processes[END_REF] for fully probabilistic processes can be smoothly adapted to the RPLTS case, and also extended to deal with ∼ PRTr and ∼ PFTr . As a consequence, we have the following spectrum under the assumption that every state has finitely many outgoing transitions.

Proposition 1. On finitely-branching RPLTS processes, it holds that: The strictness of all the inclusions above is witnessed by the counterexamples in Fig. 1. The graphical conventions for process descriptions are as follows. Vertices represent states and action-labeled edges represent action-labeled transitions. Given a transition s a -→ ∆, the corresponding a-labeled edge goes from the vertex for state s to a set of vertices linked by a dashed line, each of which represents a state s ′ ∈ supp(∆) and is labeled with ∆(s ′ ). The label ∆(s ′ ) is omitted when it is equal to 1, i.e., when ∆ is the Dirac distribution δ s ′ .

∼ PB = ∼ PS ∼ PRTr = ∼ PFTr ∼ PR = ∼ PF ∼ PCTr = ∼ PTr

Testing Equivalences for RPLTS Processes

In this section, we define a probabilistic testing equivalence for RPLTS processes under three different classes of observers respectively formalized as RPLTS, LTS, and NPLTS tests.

Given an RPLTS, we assume that the elements of its action set A are all visible. The action set of each considered test will be Ā∪{ω}, where Ā = {ā | a ∈ A} is the set of coactions for A and ω / ∈ A is a distinguished action denoting success. Every coaction must synchronize with the corresponding action; when this happens, the invisible action τ / ∈ A is produced. Therefore, the resulting interaction system is an NPLTS with action set {τ, ω}, whose transition relation -→ is derived from the transition relation -→ 1 of the RPLTS process under test and the transition relation -→ 2 of the observer, through the following two rules:

s a -→ 1 ∆ 1 o ā -→ 2 ∆ 2 (s, o) τ -→ ∆ 1 ⋆ ∆ 2 o ω -→ 2 ∆ 2 (s, o) ω -→ δ s ⋆ ∆ 2 where (∆ ⋆ Γ )(s ′ , o ′ ) = ∆(s ′ ) • Γ (o ′ ).
A finite-length computation from the initial state (s, o) of the interaction system is successful iff its last state can perform ω, and no preceding state can perform ω. Given a resolution Z of (s, o), we denote by SC(z s,o ) the set of successful computations from the state z s,o of Z corresponding to (s, o). We respectively denote by ⊔ and ⊓ the supremum and the infimum of the set of probability values prob(SC(z s,o )) computed in the various resolutions of the interaction system. To avoid infima to be trivially zero, in the next definition, which is inspired by [START_REF] Yi | Testing probabilistic and nondeterministic processes[END_REF][START_REF] Jonsson | Compositional testing preorders for probabilistic processes[END_REF][START_REF] Kwiatkowska | A testing equivalence for reactive probabilistic processes[END_REF], we restrict ourselves to maximal resolutions. Definition 4. Let L = (S, A, -→ L ) be an RPLTS. We say that s 1 , s 2 ∈ S are probabilistic ⊔⊓-testing equivalent, written s 1 ∼ PTe-⊔⊓ s 2 , iff for every test T = (O, A, -→ T ) with initial state o ∈ O it holds that:

Z1∈Resmax(s1,o) prob(SC(z s1,o )) = Z2∈Resmax(s2,o) prob(SC(z s2,o )) Z1∈Resmax(s1,o) prob(SC(z s1,o )) = Z2∈Resmax(s2,o) prob(SC(z s2,o ))
The equivalence is respectively denoted by ∼ PTe-⊔⊓,rp , ∼ PTe-⊔⊓,nd , or ∼ PTe-⊔⊓,np depending on whether the considered tests are all reactive probabilistic, fully nondeterministic, or nondeterministic and probabilistic.

We assume tests to be finite, i.e., finite state, finitely branching, and loop free. On the one hand, this entails that interaction systems will have finitely many maximal resolutions, thus ensuring the validity of our results also for a slightly finer variant of ∼ PTe-⊔⊓ that we could define following [START_REF] Segala | Testing probabilistic automata[END_REF][START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF]. On the other hand, this restriction will be exploited in the proofs of some results.

Properties of the RPLTS Testing Equivalences

Placing the Testing Equivalences in the RPLTS Spectrum

Our first result is that the three relations ∼ PTe-⊔⊓,rp , ∼ PTe-⊔⊓,nd , and ∼ PTe-⊔⊓,np are comprised between ∼ PFTr and ∼ PB . This confirms the power of the interplay between probabilities and nondeterminism for discriminating purposes, which was already noticed in the testing theory for NPLTS processes [START_REF] Jonsson | Testing and refinement for nondeterministic and probabilistic processes[END_REF][START_REF] Deng | Remarks on testing probabilistic processes[END_REF][START_REF] Bernardo | Revisiting trace and testing equivalences for nondeterministic and probabilistic processes[END_REF].

The proof that each of the three equivalences is strictly finer than ∼ PFTr benefits from an analogous result with respect to ∼ PF . Both proofs focus on tests that are deterministic LTS models (DLTS for short) as they admit neither internal nondeterminism nor probabilities. Since these tests constitute a submodel common to RPLTS, LTS, and NPLTS tests, the inclusion proofs relying on them scale to the three more expressive families of tests. Lemma 1. On RPLTS processes, for all * ∈ {rp, nd, np} it holds that: ∼ PTe-⊔⊓, * ∼ PF Theorem 1. On RPLTS processes, for all * ∈ {rp, nd, np} it holds that:

∼ PTe-⊔⊓, * ∼ PFTr
The inclusions in ∼ PFTr are strict as shown by the two RPLTS processes, the DLTS test, and the two NPLTS interaction systems in Fig. 2, because we have ⊔ = 1 and ⊓ = 0 in the first system and ⊔ = ⊓ = 0.5 in the second one.

The proof that ∼ PB is included in each of the three testing equivalences exploits the fact that ∼ PB is a congruence with respect to parallel composition. Inclusion stems from showing that, under ∼ PB , for each maximal resolution of any of the two interaction systems, there exists a maximal resolution of the other interaction system, such that the two resolutions have the same success probability. The maximal resolutions to consider are those arising from randomized ~PFTr ~PTe-,rp ~PTe-,nd ~PTe-,np schedulers, as opposed to the deterministic ones used so far, which means that a convex combination of equally labeled transitions can be selected at each state. Formally, the first clause of Def. 3 changes by requiring that, if

s 2 _ d _ g _ b _ c _ a s 1 o 1,2 1 s 1,2 o , ( ) 2 s o 1,2 ,
z a -→ Z ∆, then there exist n ∈ N ≥1 , (p i ∈ R ]0,1] | 1 ≤ i ≤ n), and (corr Z (z) a -→ L ∆ i | 1 ≤ i ≤ n) such that n i=1 p i = 1 and ∆(z ′ ) = n i=1 p i • ∆ i (corr Z (z ′ )) for all z ′ ∈ supp(∆).
Given s ∈ S, we denote by Res rnd max (s) the set of maximal resolutions of s originated from randomized schedulers. Theorem 2. On RPLTS processes, for all * ∈ {rp, nd, np} it holds that:

∼ PB ⊆ ∼ PTe-⊔⊓, *

Relationships among the RPLTS Testing Equivalences

Our second result is concerned with the relationships among the discriminating powers of ∼ PTe-⊔⊓,rp , ∼ PTe-⊔⊓,nd , and ∼ PTe-⊔⊓,np , which will help us investigating the strictness of the inclusions of Thm. 2. First of all, we observe that ∼ PTe-⊔⊓,np is included both in ∼ PTe-⊔⊓,rp and in ∼ PTe-⊔⊓,nd , because RPLTS tests and LTS tests are special cases of NPLTS tests. Both inclusions are strict, as shown in the upper part of Fig. 3, where the NPLTS test yields ⊔ = 0.75 and ⊓ = 0.25 in the first interaction system and ⊔ = ⊓ = 0.5 in the second one. We remark the need of both internal nondeterminism and probabilities in the distinguishing test. A linear test succeeding after performing ā, b, and c would not be able to tell apart s 3 and s 4 . Likewise, those two states would not be distinguishable by a test obtained from the previous one by replacing the c-transition with a probabilistic choice between that transition and a terminal/success state, or introducing a nondeterministic choice through a further b-transition to a terminal/success state after the ā-transition. Secondly, it turns out that, in general, ∼ PTe-⊔⊓,rp and ∼ PTe-⊔⊓,nd are incomparable with each other. For instance, in the middle part of Fig. 3 we have that s 5 ∼ PTe-⊔⊓,rp s 6 , while s 5 ∼ PTe-⊔⊓,nd s 6 because the LTS test yields ⊔ = 1 and ⊓ = 0 in the first interaction system and ⊔ = ⊓ = 0.5 in the second one. Notice the necessity of internal nondeterminism in the distinguishing test. In contrast, in the lower part of Fig. 3 we have that s 7 ∼ PTe-⊔⊓,nd s 8 , while s 7 ∼ PTe-⊔⊓,rp s 8 because the RPLTS test yields ⊔ = 0.75 and ⊓ = 0.25 in the first interaction system and ⊔ = ⊓ = 0.5 in the second one. Unlike the upper part of Fig. 3, here internal nondeterminism is not necessary in the distinguishing test.

Thirdly, if ∼ PTe-⊔⊓,rp admitted only restricted RPLTS tests, then it would include ∼ PTe-⊔⊓,nd , with the inclusion being strict as shown in the middle part of Fig. 3. A restricted RPLTS (RRPLTS for short) test is such that its probabilistic choices, i.e., its non-Dirac transitions, are not preceded by nondeterministic choices. The proof of this fact is based on the deprobabilization of an

a - p 2 a - a - a - 1 o 2 o n o Z Σ i i Z i . p s,o i Z Σ i i . p i Z s,o i 1 p n p T 2 T 1 T n T 2 T 1 T n o ... prob(SC(z )) = s,o prob(SC(z )) prob(SC(z )) = s,o prob(SC(z ))
... ... RRPLTS test. This is an algorithm that performs a top-down traversal of the test until a set of DLTS subtests is generated, which preserves the extremal success probabilities induced by the original test.

When encountering a non-Dirac transition in the top-down traversal of the RRPLTS test, as shown in Fig. 4 the algorithm replaces the test with as many RRPLTS subtests -which are DLTS subtests in the final steps -as there are ways of resolving the probabilistic choice. For simplicity, only the non-Dirac transition, labeled with ā, originating the probabilistic choice is depicted in the figure, but in general it could be the last transition in a computation -traversing states where no nondeterministic choices occur -going from the initial state o of the test to the probabilistic choice. Given a state s of the process under test, the two formulas in Fig. 4 witness that the two convex combinations of the extremal success probabilities induced by the n subtests respectively coincide with the two extremal success probabilities induced by the original test.

Should a nondeterministic choice precede the considered probabilistic choice, it would not be appropriate to generate subtests by resolving both choices. The reason is that it would then be natural to focus on the maximum and the minimum of the extremal success probabilities induced by the various subtests arising from the resolution of the nondeterministic choice. This certainly works when the nondeterministic choice is originated from the initial state of the test, or from the state reached by a Dirac transition of the test that synchronizes with a Dirac transition of the process under test. However, the synchronization of a Dirac transition of the test with a non-Dirac transition of the process results in a non-Dirac transition in the interaction system, for which a convex combination (as opposed to maximum and minimum) of the extremal success probabilities of the various subtests needs to be computed.

Fourthly, if ∼ PTe-⊔⊓,nd admitted only DLTS tests, then it would include ∼ PTe-⊔⊓,rp , with the inclusion being strict as shown in the lower part of Fig. 3. The reason is that a DLTS test is a special case of RPLTS test in which there are no probabilistic choices. In conclusion, we have: Theorem 3. On RPLTS processes, it holds that:

1. ∼ PTe-⊔⊓,np ∼ PTe-⊔⊓,nd and ∼ PTe-⊔⊓,np ∼ PTe-⊔⊓,rp . 2. ∼ PTe-⊔⊓,nd and ∼ PTe-⊔⊓,rp are incomparable with each other.

3. ∼ PTe-⊔⊓,nd ∼ PTe-⊔⊓,rp if only RRPLTS tests were admitted by ∼ PTe-⊔⊓,rp . 4. ∼ PTe-⊔⊓,rp ∼ PTe-⊔⊓,nd if only DLTS tests were admitted by ∼ PTe-⊔⊓,nd .

Corollary 1. On RPLTS processes, for all * ∈ {rp, nd} it holds that:

∼ PB ∼ PTe-⊔⊓, *

Open Problems and Conjectures

In this section, we address further issues related to testing equivalences for RPLTS processes. Rather than proving new results, the value of this section consists of highlighting two problems that have not received attention in the literature so far, and then proposing two conjectures for them sustained by various arguments. We hope that these discussions will help other people finding solutions to the conjectures. We expect that their proof (or their refutation) will shed light on the subtle interplay between probabilities and nondeterminism.

May Testing vs. Must Testing

In the case of testing LTS or NPLTS processes, it is known that must testing equivalence is strictly finer than may testing equivalence in the absence of divergence, otherwise the two equivalences are incomparable [START_REF] Nicola | Extensional equivalences for transition systems[END_REF][START_REF] Deng | Remarks on testing probabilistic processes[END_REF]. When testing RPLTS processes, the relationships between ∼ PTe-⊔ (may testing) and ∼ PTe-⊓ (must testing) are not clear, even if we restrict ourselves to NPLTS tests and we admit τ -actions within them.

In that case, we could derive that ∼ PTe-⊓,np ⊆ ∼ PTe-⊔,np by exploiting the construction used in [START_REF] Deng | Remarks on testing probabilistic processes[END_REF] for proving an analogous result on NPLTS processes. The purpose of that construction is to build from a given NPLTS test a dual one, which generates all complementary success probabilities in the interaction system. The idea is to transform every state of the test having an outgoing ω-transition into a terminal state, and to add to any other state a τ -transition followed by an ω-transition.

The absence of internal nondeterminism within RPLTS processes would however prevent us from concluding that the above inclusion is strict. Indeed, the typical counterexample made out of a test succeeding after performing ā followed by b, which distinguishes a process that can perform either a followed by b, or a followed by c, from a process that can perform a and then has a choice between b and c, is not applicable because the first process is not an RPLTS.

Such considerations lead us to conjecture that, for each of the three variants of ∼ PTe-⊔⊓ , its may part ∼ PTe-⊔ coincides with its must part ∼ PTe-⊓ , and hence both coincide with ∼ PTe-⊔⊓ by virtue of the definition of the latter. This is certainly true when restricting attention to fully probabilistic tests -as they yield, when interacting with an RPLTS process, a single maximal resolution, in which ⊔ and ⊓ necessarily coincide -or tests having exactly one nondeterministic choice that occurs in the initial state -as can be easily proved by induction on the number of maximal resolutions of each such test.

Conjecture 1. On RPLTS processes, for all * ∈ {rp, nd, np} it holds that:

∼ PTe-⊔, * = ∼ PTe-⊓, * = ∼ PTe-⊔⊓, *

Characterizing RPLTS Testing Equivalences

Our findings in Sect. 5 leave open the question whether ∼ PB is strictly finer than ∼ PTe-⊔⊓,np or coincides with it. In the latter case, we would have that, in the RPLTS setting, testing equivalence reaches the same discriminating power as bisimilarity not only in the presence of an explicit copying capability within tests [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], but also in the absence of it, provided that tests are equipped with both internal nondeterminism and probabilities. We point out that this would be a peculiarity of RPLTS processes, because it is known that NPLTS tests are less powerful than bisimilarity in the case of NPLTS processes [START_REF] Bernardo | Relating strong behavioral equivalences for processes with nondeterminism and probabilities[END_REF]. The numerous examples of RPLTS processes that we have examined lead us to the following:

Conjecture 2. On RPLTS processes, it holds that ∼ PTe-⊔⊓,np = ∼ PB .

As a consequence of Thm. 2, it suffices to prove that ∼ PTe-⊔⊓,np is included in ∼ PB . This is equivalent to show that, given two states s 1 and s 2 of an RPLTS, if s 1 ∼ PB s 2 , then s 1 ∼ PTe-⊔⊓,np s 2 . The idea is to build a distinguishing NPLTS test from a distinguishing formula of PML, the modal logic characterizing ∼ PB on RPLTS processes [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF]. In its minimal form [START_REF] Desharnais | Bisimulation for labelled Markov processes[END_REF], PML comprises the constant true, logical conjunction •∧•, and the diamond operator a p • where a is an action and p is a probability lower bound. Formula a p φ is satisfied by an RPLTS state if an a-labeled transition is possible from that state, after which a set of states satisfying φ is reached with probability at least p.

The proof of the conjecture appears far from being trivial. The connection between PML and the testing approach of [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] is intuitively clear, as multiplying the success probabilities resulting from the application of independent choice-free tests to as many copies of the current state under test is analogous to taking the logical conjunction of a number of formulas each starting with a suitably decorated diamond. In contrast, our tests follow the classical theory of [START_REF] De Nicola | Testing equivalences for processes[END_REF], hence do not admit any copying capability and, most importantly, may contain choices, which fit well together with logical disjunction rather than conjunction.

Nevertheless, on the basis of the examined examples, we have developed a procedure that, given an appropriate PML formula φ that is satisfied by s 1 but not s 2 , builds an NPLTS test T (φ) that should tell apart s 1 and s 2 (see Fig. 5). By appropriate PML formula, we mean that φ possesses the following three properties. First, among all the PML formulas distinguishing s 1 from s 2 , φ is one of those with the minimum depth, where the depth of a formula is the maximum number of nested diamond operators occurring in the formula itself. Second, among all the distinguishing PML formulas of minimum depth, φ is one of those with the minimum number of conjunctions. Third, all the probability lower bounds in φ are maximal, in the sense that, as soon as one of them is increased, s 1 no longer satisfies the resulting formula.

If depth(φ) = 1, then φ = a 1 true in our RPLTS setting, and hence T (φ) simply has an ā-transition followed by an ω-transition. If depth(φ) ≥ 2, then φ = a p φ ′ because the initial state of an RPLTS has a nondeterministic choice among differently labeled transitions. As a consequence, T (φ) has an ā-transition to the initial state of T ′ (φ ′ ), which is recursively built as follows.

φ depth( ') 2: i, 1 φ T'( ' ) φ i,j T'( ' ) i, 1 p p p i,j i,k i p p i,j 1 -Σ j b - n b - 1 φ T'( ') b - i i,k i φ T'( ' ) φ T'( ') b - i 1 -q depth( ') φ when = 2, φ depth( ')
If depth(φ ′ ) = 1, then φ ′ = 1≤i≤n b i 1 true, where n ∈ N ≥1 and b i1 = b i2 for i 1 = i 2 . In this case, T ′ (φ ′ ) has a nondeterministic choice among n transitions respectively labeled with b1 , b2 , . . . , bn , each followed by an ω-transition. If depth(φ ′ ) ≥ 2, then φ ′ = 1≤i≤n ( 1≤j≤ki b i pi,j φ ′ i,j ), where n ∈ N ≥1 , b i1 = b i2 for i 1 = i 2 , and k i ∈ N ≥1 for all i = 1, . . . , n with k i > 1 implying that φ ′ i,j = true for all j = 1, . . . , k i . In this case, T ′ (φ ′ ) has a nondeterministic choice among n transitions respectively labeled with b1 , b2 , . . . , bn , with the i-th transition reaching a distribution ∆ i that, for each j = 1, . . . , k i , assigns probability p i,j to the initial state of T ′ (φ ′ i,j ); whenever the various probabilities p i,j do not sum up to 1, the residual probability is assigned by ∆ i to a terminal state. Test T ′ (φ ′ i,j ) simply has an ω-transition when φ ′ i,j = true. As far as the capability of discriminating s 1 and s 2 is concerned, there are two critical points in the construction of T (φ). One of them is the last but one diamond operator occurring within each subformula of φ. Due to the minimality of φ with respect to diamond nesting depth, this is precisely a point in which a source of non-bisimilarity arises. Thus, when depth(φ ′ ) = 2, we add to T ′ (φ ′ ) a transition labeled with bi for some subformula ( 1≤j≤ki b i pi,j φ ′ i,j ) having depth 2; the transition reaches with a suitable probability q a success state (i.e., a state having an ω-transition) and with probability 1q a terminal state.

To explain the role of this additional transition, consider the two ∼ PBinequivalent states s 3 and s 4 in the upper part of Fig. 3. The conjunction-free PML formula φ = a 0.5 b 1 c 1 true is satisfied by s 3 but not s 4 . However, as argued at the beginning of Sect. 5.2, an additional transition that introduces both internal nondeterminism and a probabilistic choice between a success state and a terminal one is needed in the test to be able to distinguish s 3 and s 4 .

The other critical point is any diamond operator, preceding the last but one, which is decorated with a probability lower bound less than 1. Due to the maximality of φ with respect to probability lower bounds, this is again a point in which a source of non-bisimilarity arises. Thus, when depth(φ ′ ) ≥ 3 and the diamond operator immediately preceding φ ′ is decorated with a probability lower bound less than 1, we add to T ′ (φ ′ ) a transition labeled with bi for some subformula ( 1≤j≤ki b i pi,j φ ′ i,j ) having depth at least 3; as before, the transition reaches with a suitable probability q a state equipped with an ω-transition and with probability 1q a terminal state.

We conclude by mentioning that an alternative proof strategy for Conj. 2 may exploit Prop. 1 (∼ PB = ∼ PS ), Conj. 1, and the characterization of may testing via simulation provided by [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF]. However, we recall that in [START_REF] Deng | Characterising testing preorders for finite probabilistic processes[END_REF] τ -actions are admitted, the considered probabilistic simulation is not the standard one, and the focus is on preorders rather than equivalences.

Fig. 1 .

 1 Fig. 1. Processes illustrating the strictness of the inclusions in Prop. 1

Fig. 2 .

 2 Fig. 2. Processes and test illustrating the strictness of the inclusions of Thm. 1

Lemma 2 .

 2 Let L = (S, A, -→ L ) be an RPLTS and s 1 , s 2 ∈ S. If s 1 ∼ PB s 2 , then for every test T = (O, A, -→ T ) with initial state o ∈ O it holds that: -For each Z 1 ∈ Res rnd max (s 1 , o) there exists Z 2 ∈ Res rnd max (s 2 , o) such that: prob(SC(z s1,o )) = prob(SC(z s2,o )) -For each Z 2 ∈ Res rnd max (s 2 , o) there exists Z 1 ∈ Res rnd max (s 1 , o) such that: prob(SC(z s2,o )) = prob(SC(z s1,o ))

Fig. 3 .

 3 Fig. 3. Processes and tests illustrating the strictness of the inclusions of Thm. 3/Cor. 1

Fig. 4 .

 4 Fig. 4. Deprobabilization of an RRPLTS test (applies recursively to T1, T2, . . . , Tn)

Fig. 5 .

 5 Fig. 5. Construction of the presumably distinguishing test T (φ) based on T ′ (φ ′ )

In[START_REF] Segala | Testing probabilistic automata[END_REF], countably many different success actions are admitted but, as shown in[START_REF] Deng | Scalar outcomes suffice for finitary probabilistic testing[END_REF], the single standard one suffices in the case of finitary processes and tests.

Acknowledgment: We are grateful to the anonymous referees for their useful comments. This work is supported by MIUR-PRIN project CINA and ANR project 12IS02001 PACE.

A Proofs of Results of Sect. 5.1

Proof of Lemma 1. Since ∼ PTe-⊔⊓, * is included in ∼ PTe-⊔, * , it is sufficient to prove that the latter is included in ∼ PF . Let us restrict ourselves to consider only DLTS tests, in which neither internal nondeterminism nor probabilities are allowed, and denote by ∼ PTe-⊔,d the may part of the resulting probabilistic testing equivalence. Since a DLTS is a submodel common to RPLTS, LTS, and NPLTS, ∼ PTe-⊔, * is included in ∼ PTe-⊔,d . Thus, if we prove the inclusion in ∼ PF for the DLTS case, then the inclusion in ∼ PF will hold also for the other three cases. Given an RPLTS L = (S, A, -→) and s 1 , s 2 ∈ S, suppose that s 1 ∼ PTe-⊔,d s 2 . We first observe that s 1 ∼ PTr s 2 follows because, if it existed α ∈ A * such that prob(C(s 1 , α)) = prob(C(s 2 , α)), then a DLTS test with initial state o ′ having a single maximal computation that is labeled with ᾱ ω would violate s 1 ∼ PTe-⊔,d s 2 :

Given an arbitrary failure pair ϕ = (α, F ), with F = ∅ to avoid overlapping with ∼ PTr , we consider a DLTS test with initial state o that can only perform a computation labeled with ᾱ, after which a state is reached having an outgoing ā-transition followed by an ω-transition for each a ∈ F . For all s ∈ S and Z ∈ Res max (s, o), it holds that:

where the two values on the right do not depend on the specific resolution Z because L is an RPLTS. As a consequence, for all s ∈ S we have that:

From s 1 ∼ PTe-⊔,d s 2 and s 1 ∼ PTr s 2 it follows that:

Proof of Thm. 1. Similar to the previous proof, it is sufficient to demonstrate the inclusion of ∼ PTe-⊔,d in ∼ PFTr . Given an RPLTS L = (S, A, -→) and s 1 , s 2 ∈ S, suppose that s 1 ∼ PTe-⊔,d s 2 and consider an arbitrary failure trace φ = (a 1 , F 1 ) (a 2 , F 2 ) . . . (a n , F n ). To avoid trivial cases as well as overlapping with ∼ PTr , we assume that n ≥ 1, a i / ∈ F i-1 for all i = 2, . . . , n, and

, where a ω 2 , . . . , a ω n do not occur in L, and build a modified RPLTS M by proceeding as follows: (i) unfold up to depth n the cycles of transitions in L departing from states that can be reached within n steps from s 1 or s 2 ; (ii) for each state reachable from s 1 or s 2 after performing a computation labeled with a 1 a 2 . . . a i , 1 ≤ i ≤ n -1, and having an outgoing transition labeled with a i+1 , but no outgoing transitions labeled with actions in F i , change label a i+1 to a ω i+1 .

From s 1 ∼ PTe-⊔,d s 2 in L, it follows that s ω 1 ∼ PTe-⊔,d s ω 2 in M because the transition relabeling proceeds in the same way from both states, i.e., after performing a computation labeled with a 1 a 2 . . . a i , 1 ≤ i ≤ n -1, there is a transition to be relabeled with a ω i+1 on s 1 side iff there is an analogous transition on s 2 side. Should this not be the case for some i (which implies F i = ∅), the DLTS test that can only perform a computation labeled with ā1 ā2 . . . āi , after which a state is reached having an outgoing ā-transition followed by an ω-transition for each a ∈ F i , would tell apart s 1 and s 2 with respect to ∼ PTe-⊔,d . The reason is that one of the two states would reach success (the one in which relabeling does not take place after step i) while the other would not (the one in which relabeling takes place after step i as at that point no transition is labeled with an action in F i ). We now observe that for k = 1, 2 it holds that:

Proof of Lemma 2. Since we have to work with interaction systems that can be NPLTS models, we view L as an NPLTS so that when two states are related by ∼ PB then they are also related by the Segala & Lynch extension ∼ PB ′ relying on the following definition: an equivalence relation B over S is a probabilistic bisimulation iff, whenever (s 1 , s 2 ) ∈ B, then for all a ∈ A it holds that for each s 1 a -→ ∆ 1 there exists s 2 a -→ c ∆ 2 such that, for all equivalence classes C ∈ S/B, ∆ 1 (C) = ∆ 2 (C). The notation a -→ c stands for a combined transition labeled with a, which stems from the convex combination of a number of a-labeled transitions from the same state, i.e., from the use of a randomized scheduler. Consider an arbitrary test with state set O. Since ∼ PB ′ is a congruence with respect to parallel composition, for all s

) due to some probabilistic bisimulation B over S × O. This induces projections of B that are probabilistic bisimulations over pairs of maximal resolutions of the interaction systems. Formally, whenever

)) by proceeding by induction on the length n of the longest successful computation in the two interaction systems (notice that n is bounded because we only admit finite tests):

-If n = 0, then:

, so that o cannot perform ω, and assume that the result holds for all pairs of interaction system states that are related by a projection of B, whose successful computations have length at most n -1. For k = 1, 2 and

where the factorization of prob(SC(z s ′ ,o ′ )) with respect to the specific representative z s ′ ,o ′ of the equivalence class [z s ′ ,o ′ ] stems from the application of the induction hypothesis to all states of that equivalence class (as their successful computations have length at most n -1). Since z s ′ 1 ,o and z s ′ 2 ,o are related by the probabilistic bisimulation B 1,2 , it follows that either none of them has an outgoing transition, in which case:

)) or each of them has a single (due to the fact that resolutions are fully probabilistic) outgoing transition, say

Proof of Thm. 2. Let L = (S, A, -→ L ) be an RPLTS and s 1 , s 2 ∈ S be such that s 1 ∼ PB s 2 . By virtue of Lemma 2, for every test T = (O, A, -→ T ) with initial state o ∈ O it holds that:

prob(SC(z s2,o ))

This means that s 1 ∼ PTe-⊔⊓ s 2 because, as shown in [START_REF] Bernardo | Revisiting trace and testing equivalences for nondeterministic and probabilistic processes[END_REF], the discriminating power of ∼ PTe-⊔⊓ does not change when using randomized schedulers instead of deterministic ones.

B Proofs of Results of Sect. 5.2

Proof of Thm. 3. Let L = (S, A, -→) be an RPLTS:

1. The two inclusions immediately follow from the fact that LTS tests and RPLTS tests are special cases of NPLTS tests. 2. Incomparability stems from the middle part and the lower part of Fig. 3. 3. First of all, we establish the correctness of the deprobabilization algorithm for RRPLTS tests, i.e., the fact that the set of DLTS subtests generated by the algorithm preserves the extremal success probabilities induced by the original RRPLTS test. More precisely, given s ∈ S and an RRPLTS test T = (O, A, -→ T ) with initial state o ∈ O, it holds that:

prob(SC(z s,o ′ j )) as we prove below by proceeding by induction on the number k ∈ N ≥1 of DLTS subtests ST ′ 1 , . . . , ST ′ k with initial states o ′ 1 , . . . , o ′ k and associated probabilities q 1 , . . . , q k generated for T by the deprobabilization algorithm:

-If k = 1, then T has no non-Dirac transitions at all, and hence the only DLTS test ST ′ 1 with initial state o ′ 1 = o and associated probability 1 generated by the deprobabilization algorithm coincides with T . In this case, the result trivially holds.

-Let k ≥ 2 and assume that the result holds for all RRPLTS tests for which the deprobabilization algorithm generates at most k -1 DLTS subtests. From k ≥ 2, it follows that T has at least one non-Dirac transition. Consider the first of these transitions encountered in the top-down traversal of T , whose target distribution is supposed to assign to the states in its support the probability values p i , 1 ≤ i ≤ n, with n ∈ N ≥2 . Let ST i , 1 ≤ i ≤ n, be the corresponding RRPLTS subtests generated by the deprobabilization algorithm, with initial states o i for i = 1, . . . , n (see Fig. 4). Due to the absence in T of nondeterministic choices preceding the considered non-Dirac transition, we have that:

Since the application of the deprobabilization algorithm to each such subtest ST i generates k i ≤ k -1 DLTS subtests (which are DLTS subtests of T too) ST ′ i,h , 1 ≤ h ≤ k i , with initial states o ′ i,1 , . . . , o ′ i,ki and associated probabilities q i,1 , . . . , q i,ki , by the induction hypothesis we derive that:

)) which can be rewritten as follows due to the distributivity of multiplication with respect to addition:

Given s 1 , s