Extending Backward Compatibility of Probabilistic Testing via Coherent Resolutions?

Abstract

Testing equivalence for processes featuring both nondeterminism and probabilities is not insensitive to the moment of occurrence of nondeterministic or probabilistic choices among identical actions. Therefore, it is only partially backward compatible with testing equivalences for fully nondeterministic processes and for fully probabilistic processes. We illustrate how its backward compatibility can be extended through the joint use of coherent resolutions of nondeterminism and additional decorations for transitions, to ensure the insensitivity to the aforementioned internal choices. We also show that full backward compatibility cannot be achieved by exhibiting a counterexample with external choices too, inspired by failure semantics for fully nondeterministic processes.

-

Introduction Behavioral relations play a fundamental role in concurrency theory [ 3 ]. They formalize observational mechanisms that permit relating models that, despite their di erent representations in the same mathematical domain, cannot be distinguished by external entities when abstracting from certain internal details. Moreover, they support system modeling and veri cation by providing a means to relate system descriptions expressed at di erent levels of abstraction, as well as to reduce the size of a system representation while preserving speci c properties to be assessed later.

Several approaches to the de nition of behavioral relations have appeared in the literature, together with the investigation of their compositional, equational, and logical characteristics. Comparative concurrency theory is devoted to the study of the discriminating power and of the mutual relationships of behavioral relations. In the case of fully nondeterministic processes, from the rst work on this subject [ 15 ] to the elaboration of the full spectrum [ 22 ], a number of equivalences have emerged that range from the branching-time { i.e., (bi)simulation-based { endpoint [ 33,32 ] to the linear-time { i.e., trace-based { endpoint [ 11 ] passing through testing relations [ 16 ].

The spectrum becomes simpler when considering fully probabilistic processes [ 29,24,2 ], whereas as shown in [ 7 ] it is much more variegated in the case of processes with nondeterminism and probabilities. The reason is that only ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). after resolving nondeterminism via a scheduler it is possible to compute the probability of equivalence-speci c events. Examples of such events are reaching via given actions certain sets of equivalent states (bisimulation semantics), executing speci c action sequences (trace semantics), and passing tests formalized themselves as processes (testing semantics), with states/traces possibly being decorated with additional information.

Regardless of the speci c approach, there are at least three alternative ways of applying a behavioral equivalence to nondeterministic and probabilistic processes, based on how the resolutions of nondeterminism of those processes are compared. The three alternative ways have been addressed in the spectrum of [ 7 ]: { The rst option, coming from [ 38,36,37 ], examines the probability distributions of all equivalence-speci c events calculated over resolutions. Two processes are considered equivalent if, for each resolution of either process, there exists a resolution of the other process such that the probability of each equivalence-speci c event is the same in the two resolutions (fully matching resolutions ). The resulting portion of the spectrum closely resembles the spectrum for fully probabilistic processes. { The second option, deriving from [ 41,40,6,8 ], compares resolutions on the basis of the probabilities of individual equivalence-speci c events. A resolution of either process can be matched, with respect to di erent equivalencespeci c events, by di erent resolutions of the other process (partially matching resolutions ). The resulting equivalences are less discriminating than those arising from fully matching resolutions and retrieve nice logical characterizations for bisimilarity and compositionality properties for trace semantics. { The third option, stemming from testing theories in [ 43,27,37 ] and adapted to other semantics in [ 7 ], instead of comparing individual resolutions, takes into account only the extremal probabilities of equivalence-speci c events computed over all resolutions of the two processes (max-min matching resolutions). The resulting equivalences are less discriminating than the ones originated from partially matching resolutions, but both portions of the spectrum corresponding to these two families of equivalences feature many analogies with the spectrum for fully nondeterministic processes.

In this paper, we focus on testing semantics for nondeterministic and probabilistic processes, for which the third of the aforementioned options is the most applied one [ 43,27,37 ]. Each test is formalized as a nite nondeterministic and probabilistic process extended with success states, which is run in parallel with the process under test thus resulting in an interaction (or testing) system in which the process and the test have to synchronize on every action. The probability of reaching success is not unique, but depends on the speci c resolution of nondeterminism considered within the interaction system. In the third option above, only the two maximal resolutions respectively yielding the maximum and the minimum success probabilities are taken into account.

It is well known that behavioral equivalences for nondeterministic and probabilistic processes tend to be overdiscriminating, thereby hampering the achievement of desirable properties. For example, in [ 28,17 ] it has been shown that the testing equivalences of [ 43,27,37 ] can be characterized in terms of branching-time, simulation-like relations, which is consistent with the fact that those equivalences are not insensitive to the moment of occurrence of a nondeterministic or probabilistic choice that is internal, i.e., among identical actions. This is partly due to centralized schedulers coming into play after assembling the testing system { where a process is composed in parallel with a test, thus giving the possibility to make decisions in either component on the basis of those made in the other { which may be avoided via distributed schedulers [ 14,12,21 ]. Most importantly, it is a consequence of a special instance of the copying capability [ 1 ], which shows up in the presence of a nondeterministic choice in either component that synchonizes with a probabilistic choice in the other, thus creating copies of a state possessing several outgoing transitions where di erent decisions can be made.

This has a negative impact on the property, expected of any equivalence for nondeterministic and probabilistic processes, of being backward compatible with the corresponding equivalences for fully nondeterministic processes and for fully probabilistic processes. As recalled in [ 6 ], the testing equivalences of [ 43,27,37 ] turn out to coincide with the testing equivalence of [ 16 ] on fully nondeterministic processes only if tests are restricted to be fully nondeterministic, and with the testing equivalence of [ 13 ] on fully probabilistic processes only if tests are restricted to be fully probabilistic. The two testing equivalences of [ 16,13 ] are insensitive to internal nondeterministic or probabilistic choices, respectively.

We show that backward compatibility can be extended by making the testing equivalences of [ 43,27,37 ] insensitive to the moment in which a nondeterministic or probabilistic choice among identical actions occurs. Instead of resorting to a di erent de nition of probabilistic testing equivalence like in [ 6 ], where backward compatibility stems from comparing success probabilities in a traceby-trace fashion rather than cumulatively on all traces, we reuse the notion of coherent resolution of nondeterminism for probabilistic trace semantics developed in [ 4,5 ]. In the case of testing semantics, coherency must be accompanied by the introduction of additional transition decorations, so that the same decisions are made by schedulers in distinct copies of the same state of a process or a test occurring in a choice within the testing system. This is similar to the technique employed in [ 20 ] for processes in which action, nondeterministic, and probabilistic branchings alternate, with the remarkable di erence that our decoration procedure is much simpler. Consistent with the ready-trace semantics characterization of [ 20 ], a counterexample inspired by failure semantics for fully nondeterministic processes shows that full backward compatibility cannot be achieved in the presence of certain synchronizations among external choices.

This paper is organized as follows. In Sect. 2, we recall background de nitions for nondeterministic and probabilistic processes as well as resolutions of nondeterminism. In Sect. 3, we present testing equivalence for those processes together with its limitations about backward compatibility. In Sect. 4, we illustrate an adaptation of coherent resolutions to testing systems in which transitions are suitably decorated, so as to gain insensitivity to the moment of occurrence of internal nondeterministic or probabilistic choices. This results in a higher level of backward compatibility with respect to [ 43,27,37 ]. 2

Nondeterministic and Probabilistic Processes Processes featuring nondeterminism and probability are typically described by extending the labeled transition system (LTS) model [ 30 ] in such a way that every action-labeled transition goes from a source state to a probability distribution over target states [ 31,35 ] rather than to a single target state. These models are essentially Markov decision processes [ 19 ], or probabilistic automata in the sense of [ 34 ], that additionally allow for internal nondeterminism, i.e., equally labeled transitions departing from the same state.

In the literature, they have been represented through a number of slightly di erent probabilistic computational entities such as, e.g., concurrent Markov chains [ 42 ], strictly alternating models [ 23 ], probabilistic automata in the sense of [ 35 ], and the denotational probabilistic models of [ 25 ]; see [ 39 ] for an overview. We formalize them through a variant of simple probabilistic automata [ 35 ], in which we do not distinguish between external and internal actions. De nition 1. A nondeterministic and probabilistic labeled transition system, NPLTS for short, is a triple (S; A; !) where S 6= ; is an at most countable set of states, A 6= ; 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! . We say that s0 2 S is not reachable from s via that a-transition if (s0) = 0, otherwise we say that it is reachable with probability p = (s0). The reachable states form the support of the target distribution , i.e., supp( ) = fs0 2 S j (s0) > 0g. An NPLTS can be depicted as a directed graph in which vertices represent states and action-labeled edges represent transitions, with states in the support of the same target distribution being linked by a dashed line and decorated with the respective probabilities when these are di erent from 1 (see the forthcoming Figs. 1 to 4).

The nondeterministic choice among all the transitions departing from state s can be in uenced by the external environment, while the probabilistic choice of the target state for a speci c outgoing transition of s takes place internally. An NPLTS represents a fully nondeterministic process when every transition has a target distribution with a singleton support, while it represents a fully probabilistic process when every state has at most one outgoing transition.

In this setting, a computation is a sequence of state-to-state steps, each denoted by s a7! s0 and derived from a state-to-distribution transition s a! . De nition 2. Let L = (S; A; nite sequence of steps:

a1 a2 an c s0 7! s1 7! s2 : : : sn 1 7! sn is a computation of L of length n 2 N from s = s0 to s0 = sn compatible with !) be an NPLTS and s; s0 2 S. We say that the trace = a1 a2 : : : an 2 A , written c 2 CC(s; ), i for each step si 1 a7!i si in c there is a transition si 1 a!i i in L such that si 2 supp( i), 1 i n, where: { i(si) is the execution probability of step si 1 a7!i si conditioned on the selection of transition si 1 a!i i at state si 1, or simply the execution probability of that step if L is fully probabilistic. { prob(c) = Q1 i n i(si) is the execution probability of c if L is fully probabilistic, assuming prob(c) = 1 when n = 0. { For C CC(s; ), we let prob(C) = Pc2C prob(c) if L is fully probabilistic, provided that no computation in C is a proper pre x of one of the others.

When several transitions depart from the same state s of an NPLTS L, they describe a nondeterministic choice among di erent behaviors. A resolution of s is the result of a possible way of resolving nondeterministic choices starting from s, as if a scheduler were applied that decides which activity has to be performed next. A resolution of nondeterminism can thus be formalized as a fully probabilistic NPLTS Z with a tree-like structure, whose branching points correspond to target distributions of transitions deriving from those of L.

There are two ways of resolving nondeterminism. The structure-preserving approach constructs a resolution by importing states and transitions from the original NPLTS via a deterministic scheduler. In a resolution of the structuremodifying approach, (i) a transition can be produced by probabilistically combining transitions of the original model via a randomized scheduler [ 35 ], or (ii) a state can be obtained by probabilistically splitting states of the original model via an interpolating scheduler [ 18 ], or (iii) a combination thereof [ 10 ].

In this paper, we focus on structure-preserving resolutions arising from centralized, memoryless, deterministic schedulers. At each step, a scheduler of this kind selects one of the transitions departing from the current state, or no transitions at all thus stopping the execution. As a consequence, the resulting resolution is isomorphic to a submodel of the original model (or of its unfolding, should cycles be present), thereby preserving the structure of the original model (or of its unfolding). If the model is fully nondeterministic, each of its resolutions coincides with a computation of the model; if the model is fully probabilistic, its maximal resolution coincides with (the unfolding of) the entire model.

Following [ 26,9 ] we introduce a correspondence function corrZ : Z ! S from the acyclic state space of the resolution Z = (Z; A; !Z ) being built, to the possibly cyclic state space of the considered model L = (S; A; !L). For each transition z a!Z , the function corrZ must preserve the probabilities of all the states corresponding to those in supp( ) and must be injective over supp( ). In the absence of injectivity, the original structure may not be preserved in the case that the target distribution of a transition assigns the same probability to several inequivalent states. This is exempli ed in Fig. 1. The correspondence function that maps z to s, z10 and z20 to s01, and z100 and z200 to s010 would cause the rightmost NPLTS to be considered a legal resolution of the leftmost NPLTS, which is not correct as the former is not isomorphic to any submodel of the latter.

0.5 De nition 3. Let L = (S; A; !L) be an NPLTS and s 2 S. An acyclic NPLTS Z = (Z; A; !Z ) is a structure-preserving resolution of s, written Z 2 Ressp(s), i there exists a correspondence function corrZ : Z ! S such that s = corrZ (zs), for some zs 2 Z acting as the initial state of Z, and for all z 2 Z it holds that: { If z a!Z then corrZ (z) a!L , with corrZ being injective over supp( ) and satisfying (z0) = (corrZ (z0)) for all z0 2 supp( ).

{ At most one transition departs from z.

Z is maximal, written Z 2 Ressp;max(s), i for all z 2 Z, whenever z has no outgoing transitions, then corrZ (z) has no outgoing transitions either. 3

Partial Compatibility of NPLTS Testing Equivalence The testing theories developed in [ 43,27,37 ] for nondeterministic and probabilistic processes are based on comparing the extremal probabilities of passing a test. We formalize both processes and tests as NPLTS models, with the di erence that a test has nitely many states and transitions, features an acyclic graph structure, and may contain occurrences of a success state. A test is passed by a process with a certain probability if there exists a resolution of nondeterminism of the parallel composition of the process and the test, with synchronization being enforced on any action, in which the probability of reaching a state having success in its test component is equal to the given probability.

De nition 4. A nondeterministic and probabilistic test, NPT for short, is an acyclic NPLTS T = (O; A; !) where both O and ! are nite, with O containing a distinguished success state denoted by ! having no outgoing transitions. We say that a computation of T is successful i its last state is !. De nition 5. Let L = (S; A; !L) be an NPLTS and T = (O; A; !T ) be an NPT. The interaction system of L and T is the NPLTS I(L; T ) = (S O; A; !) where: { Every (s; o) 2 S O is called a con guration, which is successful i o = !. { (s; o) a! i s a!L 1 and o a!T 2 with (s0; o0) = 1(s0) 2(o0) for all (s0; o0) 2 S O. { A computation of I(L; T ) is successful i so is its last con guration.

We observe that I(L; T ) and any Z 2 Ressp(s; o) have nitely many computations due to the test structure; we denote by SC(zs;o) the set of successful computations from the initial state zs;o of Z. Only maximal resolutions of nondeterminism are taken into account within interaction systems, because the ones that are not maximal do not expose all successful computations and hence may erroneously lead to conclude that the minimal success probability is zero. We respectively denote by t and u the supremum and in mum of a set of numbers. De nition 6. Let L = (S; A; !L) be an NPLTS. States s1; s2 2 S are probabilistic testing equivalent, written s1 PTe-tu s2, i for every NPT T = (O; A; !T ) with initial state o 2 O it holds that:

F prob(SC(zs1;o)) = F prob(SC(zs2;o))

As shown in Thm. 4:4 of [ 6 ], the discriminating power of PTe-tu does not change if randomized schedulers are used in place of deterministic ones. As further shown in Thm. 4:8 of [ 6 ], PTe-tu is backward compatible with the testing equivalence of [ 16 ] on fully nondeterministic processes (in the sense that the two equivalences coincide on those processes) only if tests are restricted to be fully nondeterministic in PTe-tu. Likewise, PTe-tu is backward compatible with the testing equivalence of [ 13 ] on fully probabilistic processes only if tests are restricted to be fully probabilistic in PTe-tu. We recall below the de nition of testing equivalence for the two considered classes of processes.

De nition 7. Let L = (S; A; !L) be a fully nondeterministic NPLTS. States s1; s2 2 S are fully nondeterministic testing equivalent, written s1 FNDTe s2, i for every fully nondeterministic NPT T = (O; A; !T ) with initial state o 2 O it holds that: { There exists a successful computation from (s1; o) i there exists a successful computation from (s2; o) { known as may testing. { All maximal computations from (s1; o) are successful i all maximal computations from (s2; o) are successful { known as must testing.

De nition 8. Let L = (S; A; !L) be a fully probabilistic NPLTS. States s1; s2 2 S are fully probabilistic testing equivalent, written s1 FPTe s2, i for every fully probabilistic NPT T = (O; A; !T ) with initial state o 2 O it holds that: prob(SC(s1; o)) = prob(SC(s2; o))

The reason for the aforementioned incompleteness of backward compatibility can be illustrated through some counterexamples. For the two fully nondeterministic NPLTS models in Fig. 2(A) whose initial states are s1 and s2, it is well known that s1 FNDTe s2, but s1 6 PTe-tu s2 because the fully probabilistic s1 a a s2 a s’ 2 b b d c zs’1,o

zs"1,o

(s1,o) 1−p

p b b (r1,u) a b 1−p

p b c ω b c ω Fig. 2. (A) Two FNDTe-equivalent fully nondeterministic NPLTS models that are

PTe-tu-distinguished by a fully probabilistic test. (B) Two FPTe-equivalent fully probabilistic NPLTS models PTe-tu-distinguished by a fully nondeterministic test. In both cases, an internal nondeterministic choice on b synchronizes with an internal probabilistic choice on b. This originates copies of the same state in the corresponding interaction systems, as well as sensitivity to the moment of occurrence of the internal choice in the original systems under test. zs"2",o a b copy 1−p (r"2,u’) b

d ω zr"2",u a b b ω

d b ω d p 1−p p 1−p p 1−p p

1−p not coherent

d cohneortent p 1−p p 1−p p 1−p p

1−p not coherent

d cohneortent NPT with initial state o tells them apart. Assuming p 1 p, the interaction system with initial state (s1; o) has two maximal resolutions yielding t = p and u = 1 p, while the interaction system with initial state (s2; o) has four maximal resolutions yielding t = 1 and u = 0 instead. The synchronization of the nondeterministic choice between the two b-transitions reachable from s2 with the probabilistic choice between the two b-transitions reachable from o creates two copies of state s02 in the second interaction system. The same internal nondeterministic choice is enabled in either copy, thereby giving the scheduler the opportunity of performing the incoherent selections that lead to the two maximal resolutions respectively yielding t = 1 and u = 0.

The situation is similar in Fig. 2(B) with the two FPTe-equivalent fully probabilistic NPLTS models whose initial states are r1 and r2. They are distinguished with respect to PTe-tu by the fully nondeterministic NPT whose initial state is u. This is due to the two copies of u0 in the second interaction system, in each of which the same internal nondeterministic choice is enabled. 4

Extending Compatibility via Coherent Resolutions The anomalies shown in Fig. 2 are due to the freedom of schedulers of making di erent decisions in states enabling the same actions. For these situations, in [ 4 ] we proposed to limit the excessive power of schedulers by restricting them to yield coherent resolutions. Intuitively, this means that, if several states in the support of the target distribution of a transition are equivalent, then the decisions made by the scheduler in those states have to be coherent with each other, so that the states to which they correspond in any resolution are equivalent too. Although developed for trace semantics, we now show that the notion of coherent resolution applies to testing semantics as well.

The restriction to coherent maximal resolutions of interaction systems is the basis for developing a variant cPTe-tu of probabilistic testing equivalence whose backward compatibility with FNDTe and FPTe is higher than PTe-tu. Similar to [ 20 ], in addition to coherency, within resolutions of interaction systems we need suitable decorations to di erentiate among identically labeled transitions departing from states deriving from copies of a state of the process or the test.

In Fig. 2, for instance, both states (s02; o0) and (s02; o00) embody a copy of s02. Therefore, with respect to a scheduler, in those two states only the choice of their two left b-transitions or right b-transitions should be considered coherent, which can be achieved by decorating in the same way corresponding transitions departing from the two considered states. The situation is similar for (r20; u0) and (r200; u0), with the di erence that the state being copied comes from the test.

Unlike [ 20 ], our decoration procedure is very simple. The decoration of each transition of the process and of the test is just a serial number, then each transition of the interaction system inherits the serial numbers of the two transitions from which it is originated. This is illustrated in Fig. 3, where in the maximal resolution whose initial state is zs02;o the two b-transitions are coherent with each other because they both derive from the b-transition of s02 decorated with 1, while s1 a a 0 1 b b 2 3 s2 this is not the case in the maximal resolution whose initial state is zs002;o because the two b-transitions respectively stem from the two b-transitions of s0 . 2

The coherency constraints behind the formalization of coherent resolutions have been introduced in [ 4 ]. They rely on coherent trace distributions, which are suitable families of sets of traces weighted with their execution probabilities in a given resolution, built through the following operations. To take decorations into account, which we assume to be unique within any NPLTS, we replace A with B = A N N and adapt de nitions accordingly. with: De nition 9. For b 2 B, p 2 R, TD 2B R, and T B R we de ne: b : TD = fb : T j T 2 TDg b : T = f(b ; p0) j ( ; p0) 2 T g p TD = fp T j T 2 TDg p T = f( ; p p0) j ( ; p0) 2 T g dtr(TD) = fdtr(T ) j T 2 TDg dtr(T ) = f 2 B j 9p0 2 R: ( ; p0) 2 T g while for TD1; TD2 2B R we de ne: >8 fT1 + T2 j T1 2 TD1 ^ T2 2 TD2 ^ dtr(T1) dtr(T2)g <> if dtr(TD1) dtr(TD2) TD1 + TD2 = > fT1 + T2 j T1 2 TD1 ^ T2 2 TD2g >: otherwise where for T1; T2 B R we de ne: T1 + T2 = f( 1; p1 + p2) j ( 1; p1) 2 T1 ^ ( 2; p2) 2 T2 ^ 1 2g [ f( ; p) 2 T1 [ T2 j there is no ( ; q) in the other trace set s.t. g { 1 2 i either 1 = 2 = ", or 1 = ha; h1; k1i 10, 2 = ha; h2; k2i 20, h1 = h2 _ k1 = k2, and 10 20. { dtr(T1) dtr(T2) i for each 1 2 dtr(T1) there exists 2 2 dtr(T2) such that 1 2, and vice versa. { dtr(TD1) dtr(TD2) i for each T1 2 TD1 there exists T2 2 TD2 such that dtr(T1) dtr(T2), and vice versa.

Weighted trace set addition T1 + T2 is commutative and associative, with probabilities of equivalent traces in the two summands being always added up for coherency purposes. In constrast, trace distribution addition is only commutative. Essentially, the two summands in TD1 + TD2 represent two families of sets of weighted traces executable in the resolutions of two states in the support of a target distribution. Every weighted trace set T1 2 TD1 is summed with every weighted trace set T2 2 TD2 { so as to characterize an overall resolution { unless TD1 and TD2 have equivalent families of trace sets, in which case summation is restricted to weighted trace sets featuring equivalent traces for the sake of coherency. Due to the lack of associativity, in the de nition below all trace distributions (s0) TDcn 1(s0) exhibiting a trace set family equivalent to have to be summed up rst, which is ensured by the presence of a double summation. De nition 10. Let (S; B; !) be an NPLTS and s 2 S. The coherent decorated trace distribution of s is the subset of 2B R]0;1] de ned as follows:

TDc(s) = Sn2N TDcn(s) with the coherent decorated trace distribution of s whose traces have length at most n, i.e., TDcn(s), being de ned as: 8 >>>>>< ("; 1) y s a;Sh!;k ha; h; ki : dtr(TDcn 1(s0)) !

P P (s0) TDcn 1(s0) 2dtr( ;n 1) s02supp( )

if n > 0 and s has outgoing transitions > >>>> ff("; 1)gg : otherwise where dtr( ; n 1) = fdtr(TDcn 1(s0)) j s0 2 supp( )g and the operator ("; 1) y is such that ("; 1) y TD = ff("; 1)g [ T j T 2 TDg.

As shown by several examples in [ 4 ], the coherency constraints should involve all TDn( ) distributions separately { rather than TDc( ) { and should not c consider the probabilities contained in those trace distributions { which are instead necessary for alternative characterizations of probabilistic trace semantics. In [ 5 ] it was further shown that the coherency constraints should be based on a monotonic construction in which any TDcn( ) incrementally builds on TDcn 1( ), in the sense that every weighted trace set in the former should include as a subset a weighted trace set in the latter. This is achieved through a fully coherent variant of trace distribution, which we adapt below.

De nition 11. Let (S; B; !) be an NPLTS and s 2 S. The fully coherent decorated trace distribution of s is the subset of 2B R]0;1] de ned as follows:

TDfc(s) = Sn2N TDfnc(s) with the fully coherent decorated trace distribution of s whose traces have length at most n being the subset of TDcn(s) de ned as:

8> fT 2 TDcn(s) j 9T 0 2 TDfnc 1(s): T 0 T g TDfnc(s) = >< if n > 0 and s has outgoing transitions > ff("; 1)gg >: otherwise

Since testing semantics makes use of maximal resolutions only, with respect to [ 4,5 ] the rst coherency constraint su ces and is adapted as follows. De nition 12. Let L = (S; B; !L) be an NPLTS, s 2 S, Z = (Z; B; !Z ) 2 Ressp;max(s) with correspondence function corrZ : Z ! S. We say that Z is a coherent maximal resolution of s, written Z 2 Resscp;max(s), i for all z 2 Z, whenever z a;h!;kZ , then for all n 2 N and z0; z00 2 supp( ) it holds that: dtr(TDfnc(corrZ (z0))) dtr(TDfnc(corrZ (z00))) =) dtr(TDfnc(z0)) dtr(TDfnc(z00)) !) where (s; o) a;h;k

! 2(o0) for all (s0; o0) 2 S i s O.

I(L; T ) = (S (s0; o0) =

O; B; 1(s0) De nition 14. Let L = (S; A N; !L) be an NPLTS. States s1; s2 2 S are coherent probabilistic testing equivalent, written s1 cPTe-tu s2, i for every NPT T = (O; A N; !T ) with initial state o 2 O it holds that:

F prob(SC(zs1;o)) = F prob(SC(zs2;o))

Z12Resscp;max(s1;o)

d

Z12Resscp;max(s1;o)

As an example, dtr(TDf1c(s02; o0)) = ff"; hb; 1; 1ig; f"; hb; 2; 1igg is identi ed via with dtr(TDf1c(s02; o00)) = ff"; hb; 1; 2ig; f"; hb; 2; 2igg, hence the states to which they correspond in any coherent maximal resolution of (s2; o) must result in an analogous identi cation. In contrast, hb; 1; 1i cannot be identi ed with hb; 2; 2i because 1 = h1 6= h2 = 2 and 1 = k1 6= k2 = 2. Likewise, hb; 2; 1i cannot be identi ed with hb; 1; 2i because 2 = h1 6= h2 = 1 and 1 = k1 6= k2 = 2. As a consequence, the two maximal resolutions of (s2; o) in Fig. 2 respectively having initial states zs002;o and zs0020;o and success probabilities 1 and 0, with the former appearing also in Fig. 3 together with its decorations, are not coherent. It thus turns out that s1 cPTe-tu s2; for similar reasons, r1 cPTe-tu r2.

We nally prove that the joint use of coherency and decorations makes cPTe-tu insensitive to the moment of occurrence of internal nondeterministic or probabilistic choices. Before that, we show that full backward compatibility with FNDTe and FPTe cannot be achieved, though. Consider the two fully nondeterministic NPLTS models with initial states t1 and t2 in Fig. 4. These two models are known to be failure equivalent, i.e., identi ed by the must-part of FNDTe [ 15 ], hence we may expect them to be identi ed by cPTe-tu too. However, this is not the case, as witnessed by the fully probabilistic NPT with initial state w because of the maximal resolution of (t2; w) with success probability 1, in which the (external) nondeterministic choice between the b-transition and the c-transition after the central a-transition of t2 synchronizes with the (external) probabilistic choice between the b-transition and the c-transition departing from the two states in the support of the a-transition of w.

The backward compatibility of cPTe-tu extends till the point in which the following property Sext holds: whenever an external nondeterministic choice of the process (resp. test) synchronizes with an external probabilistic choice of the test (resp. process), then all the states in the support of the target distribution of the resulting (interaction system) transition enable the same set of actions. Theorem 1. Let L = (S; A N; !L) be an NPLTS and admit only NPTs T = (O; A N; !T ) such that I(L; T ) = (S O; B; !) meets Sext. For s1; s2 2 S: 1. If L is fully nondeterministic, then s1 cPTe-tu s2 () s1 FNDTe s2. 2. If L is fully probabilistic, then s1 cPTe-tu s2 () s1 FPTe s2.

References

1. S. Abramsky . Observational equivalence as a testing equivalence . Theoretical Computer Science , 53 : 225 { 241 , 1987 .

2. C. Baier , J.-P. Katoen , H. Hermanns , and V. Wolf . Comparative branching-time semantics for Markov chains . Information and Computation , 200 : 149 { 214 , 2005 .

3. J.A. Bergstra , A. Ponse , and S.A . Smolka (editors). Handbook of Process Algebra. Elsevier , 2001 .

4. M. Bernardo . Coherent resolutions of nondeterminism . In Proc. of the 16th European Performance Engineering Workshop (EPEW 2019 ), volume 12039 of LNCS , pages 16 { 32 . Springer, 2019 .

5. M. Bernardo . Alternative characterizations of probabilistic trace equivalences on coherent resolutions of nondeterminism . In Proc. of the 17th Int. Conf. on the Quantitative Evaluation of Systems (QEST 2020 ), LNCS. Springer, 2020 . To appear.

6. M. Bernardo , R. De Nicola, and M. Loreti . Revisiting trace and testing equivalences for nondeterministic and probabilistic processes . Logical Methods in Computer Science , 10 ( 1 :16): 1 { 42 , 2014 .

7. M. Bernardo , R. De Nicola, and M. Loreti . Relating strong behavioral equivalences for processes with nondeterminism and probabilities . Theoretical Computer Science , 546 : 63 { 92 , 2014 .

8. M. Bernardo , R. De Nicola, and M. Loreti . Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes . Acta Informatica , 52 : 61 { 106 , 2015 .

9. M. Bernardo , D. Sangiorgi , and V. Vignudelli . On the discriminating power of testing equivalences for reactive probabilistic systems: Results and open problems . In Proc. of the 11th Int. Conf. on the Quantitative Evaluation of Systems (QEST 2014 ), volume 8657 of LNCS , pages 281 { 296 . Springer, 2014 .

10. F. Bonchi , A. Sokolova , and V. Vignudelli . The theory of traces for systems with nondeterminism and probability . In Proc. of the 34th ACM/IEEE Symp. on Logic in Computer Science (LICS 2019 ), pages ( 19 :62)1{ 14 . IEEE-CS Press, 2019 .

11. S.D. Brookes , C.A.R. Hoare , and A.W. Roscoe . A theory of communicating sequential processes . Journal of the ACM , 31 : 560 { 599 , 1984 .

12. L. Cheung , N.A. Lynch , R. Segala , and F. Vaandrager . Switched PIOA: Parallel composition via distributed scheduling . Theoretical Computer Science , 365 : 83 { 108 , 2006 .

13. R. Cleaveland , Z. Dayar , S.A. Smolka , and S. Yuen . Testing preorders for probabilistic processes . Information and Computation , 154 : 93 { 148 , 1999 .

14. L. de Alfaro, T.A. Henzinger , and R. Jhala . Compositional methods for probabilistic systems . In Proc. of the 12th Int. Conf. on Concurrency Theory (CONCUR 2001 ), volume 2154 of LNCS , pages 351 { 365 . Springer, 2001 .

15. R. De Nicola. Extensional equivalences for transition systems . Acta Informatica , 24 : 211 { 237 , 1987 .

16. R. De Nicola and M. Hennessy . Testing equivalences for processes . Theoretical Computer Science , 34 : 83 { 133 , 1984 .

17. Y. Deng , R.J. van Glabbeek , M. Hennessy , and C. Morgan . Characterising testing preorders for nite probabilistic processes . Logical Methods in Computer Science , 4 ( 4 :4):1{ 33 , 2008 .

18. Y. Deng , R.J. van Glabbeek, C. Morgan , and C. Zhang. Scalar outcomes su ce for nitary probabilistic testing . In Proc. of the 16th European Symp. on Programming (ESOP 2007 ), volume 4421 of LNCS , pages 363 { 378 . Springer, 2007 .

19. C. Derman. Finite State Markovian Decision Processes . Academic Press, 1970 .

20. S. Georgievska and S. Andova . Probabilistic may/must testing: Retaining probabilities by restricted schedulers . Formal Aspects of Computing , 24 : 727 { 748 , 2012 .

21. S. Giro and P.R. D'Argenio . On the expressive power of schedulers in distributed probabilistic systems . In Proc. of the 7th Int. Workshop on Quantitative Aspects of Programming Languages (QAPL 2009 ), volume 253 ( 3 ) of ENTCS , pages 45 { 71 . Elsevier , 2009 .

22. R.J. van Glabbeek. The linear time { branching time spectrum I. In Handbook of Process Algebra , pages 3 { 99 . Elsevier , 2001 .

23. H. Hansson and B. Jonsson . A calculus for communicating systems with time and probabilities . In Proc. of the 11th IEEE Real-Time Systems Symp. (RTSS 1990 ), pages 278 { 287 . IEEE-CS Press, 1990 .

24. D.T. Huynh and L. Tian . On some equivalence relations for probabilistic processes . Fundamenta Informaticae , 17 : 211 { 234 , 1992 .

25. H. Jifeng , K. Seidel , and A. McIver . Probabilistic models for the guarded command language . Science of Computer Programming , 28 : 171 { 192 , 1997 .

26. B. Jonsson , C. Ho-Stuart , and Wang Yi . Testing and re nement for nondeterministic and probabilistic processes . In Proc. of the 3rd Int. Symp. on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT 1994 ), volume 863 of LNCS , pages 418 { 430 . Springer, 1994 .

27. B. Jonsson and Wang Yi . Compositional testing preorders for probabilistic processes . In Proc. of the 10th IEEE Symp. on Logic in Computer Science (LICS 1995 ), pages 431 { 441 . IEEE-CS Press, 1995 .

28. B. Jonsson and Wang Yi . Testing preorders for probabilistic processes can be characterized by simulations . Theoretical Computer Science , 282 : 33 { 51 , 2002 .

29. C.-C. Jou and S.A. Smolka . Equivalences, congruences, and complete axiomatizations for probabilistic processes . In Proc. of the 1st Int. Conf. on Concurrency Theory (CONCUR 1990 ), volume 458 of LNCS , pages 367 { 383 . Springer, 1990 .

30. R.M. Keller. Formal veri cation of parallel programs . Communications of the ACM , 19 : 371 { 384 , 1976 .

31. K.G. Larsen and A. Skou . Bisimulation through probabilistic testing . Information and Computation , 94 :1{ 28 , 1991 .

32. R. Milner . Communication and Concurrency. Prentice Hall, 1989 .

33. D. Park . Concurrency and automata on in nite sequences . In Proc. of the 5th GI Conf. on Theoretical Computer Science , volume 104 of LNCS , pages 167 { 183 . Springer, 1981 .

34. M.O. Rabin . Probabilistic automata . Information and Control , 6 : 230 { 245 , 1963 .

35. R. Segala . Modeling and Veri cation of Randomized Distributed Real-Time Systems . PhD Thesis , 1995 .

36. R. Segala . A compositional trace-based semantics for probabilistic automata . In Proc. of the 6th Int. Conf. on Concurrency Theory (CONCUR 1995 ), volume 962 of LNCS , pages 234 { 248 . Springer, 1995 .

37. R. Segala . Testing probabilistic automata . In Proc. of the 7th Int. Conf. on Concurrency Theory (CONCUR 1996 ), volume 1119 of LNCS , pages 299 { 314 . Springer, 1996 .

38. R. Segala and N.A. Lynch . Probabilistic simulations for probabilistic processes . In Proc. of the 5th Int. Conf. on Concurrency Theory (CONCUR 1994 ), volume 836 of LNCS , pages 481 { 496 . Springer, 1994 .

39. A. Sokolova and E.P. de Vink. Probabilistic automata: System types, parallel composition and comparison . In Validation of Stochastic Systems , volume 2925 of LNCS , pages 1 { 43 . Springer, 2004 .

40. L. Song , L. Zhang , J.C. Godskesen , and F. Nielson . Bisimulations meet PCTL equivalences for probabilistic automata . Logical Methods in Computer Science , 9 ( 2 :7):1{ 34 , 2013 .

41. M. Tracol , J. Desharnais , and A. Zhioua . Computing distances between probabilistic automata . In Proc. of the 9th Int. Workshop on Quantitative Aspects of Programming Languages (QAPL 2011 ), volume 57 of EPTCS , pages 148 { 162 , 2011 .

42. M.Y. Vardi . Automatic veri cation of probabilistic concurrent nite-state programs . In Proc. of the 26th IEEE Symp. on Foundations of Computer Science (FOCS 1985 ), pages 327 { 338 . IEEE-CS Press, 1985 .

43. Wang Yi and K.G. Larsen . Testing probabilistic and nondeterministic processes . In Proc. of the 12th Int. Symp. on Protocol Speci cation, Testing and Veri cation (PSTV 1992 ), pages 47 { 61 . North-Holland, 1992 .