1 Introduction

Quantitative models of computer, communication, and software systems combine, among others, functional and extra-functional aspects of system behavior. On the one hand, these models describe system activities and their execution order, possibly admitting nondeterminism in case of concurrency phenomena or to support implementation freedom. On the other hand, they include some information about the probabilities or the timing of activities and events in which the system is involved.

In the probabilistic setting, a particularly expressive model is given by probabilistic automata  [24], because they encompass as special cases fully nondeterministic models like labeled transition systems  [21], fully probabilistic models like action-labeled variants of discrete-time Markov chains  [22], and reactive probabilistic models like Markov decision processes  [13]. In a probabilistic automaton, the choice among the transitions departing from the current state is nondeterministic and can be influenced by the external environment, while the choice of the next state reached by the selected transition is probabilistic and made internally by the process.

Behavioral relations  [1, 4, 16, 20, 28] play a fundamental role in the analysis of probabilistic models. They formalize observational mechanisms that permit relating models that, despite their different representations in the same mathematical domain, cannot be distinguished by external entities when abstracting from certain internal details. Moreover, they support system modeling and verification by providing a means to relate system descriptions expressed at different levels of abstraction, as well as to reduce the size of a system representation while preserving specific properties to be assessed later.

In this paper, we focus on trace semantics for nondeterministic and probabilistic processes represented through a variant of simple probabilistic automata. A trace is a sequence of activities labeling a sequence of transitions performed by a process, thus abstracting from branching points in the process behavior. Several execution probabilities may be associated with the same trace, each corresponding to a different resolution of nondeterminism. The discriminating power of probabilistic trace semantics thus depends on the class of schedulers used to resolve nondeterminism, but in general it turns out to be excessive. This may hamper the achievement of a number of desirable properties.

The problem with almighty schedulers yielding a demonic view of nondeterminism is well known, both for trace semantics and for testing semantics. In the case of a process given by the parallel composition of several subprocesses, or in a testing scenario where a process is composed in parallel with a test, schedulers come into play after assembling the various components. As a consequence, schedulers can solve both choices local to the individual subprocesses and choices arising from their interleaving execution. This centralized approach thus gives the possibility to make decisions in one component on the basis of those made in other components, especially in the case of history-dependent schedulers  [30].

To cope with the aforementioned information leakage, the idea of distributed scheduling was proposed in  [10]. Given a number of modules, i.e., of variable-based versions of automata, that interact synchronously by updating all variables during every round, for each module there are several schedulers. One of them chooses the initial and updated values for the module external variables; for each atom, intended as a cluster of variables of the module, a further scheduler chooses the initial and updated values for the private and interface variables controlled by that atom. Compose-and-schedule is thus replaced by schedule-and-compose.

Distributed scheduling was then applied in  [9] to the asynchronous model of switched probabilistic input/output automata. Following the terminology of  [29], given a reactive interpretation to input actions and a generative interpretation to output actions, an input scheduler and an output scheduler are considered for each automaton occurring in a system. A token passing mechanism among the automata eliminates global choices by ensuring that a single automaton at a time can select a generative output action, to which the other automata can respond with reactive input actions having the same name.

Both  [10] and  [9] guarantee the compositionality of the probabilistic trace-distribution equivalence of  [25]. This is not a congruence with respect to parallel composition under centralized scheduling; as shown in  [23], the coarsest congruence contained in that linear-time equivalence turns out to be a variant of the simulation equivalence of  [27], which is a branching-time equivalence. Distributed scheduling was further investigated in  [15] for interleaved probabilistic input/output automata, a variant of switched ones in which an interleaving scheduler replaces the token passing mechanism. The examined problem was the attainment of the extremal probabilities of satisfying reachability properties under different classes of distributed schedulers (memoryless vs. history-dependent, deterministic vs. randomized), knowing that in the centralized case those probabilities are obtained when using memoryless deterministic schedulers  [6].

Indeed, the overwhelming power of schedulers already shows up in the memoryless case, i.e., when neglecting the path followed to reach the current state. Under centralized scheduling, in  [14] additional labels were used so that the same decisions are made by schedulers in distinct copies of the same state of a testing system, thus weakening the discriminating power of the probabilistic testing equivalences of  [18, 26, 31] that, as shown in  [11, 19], can be characterized in terms of branching-time, simulation-like relations. An analogous weakening result under the same class of schedulers was obtained in  [3] by means of a different definition of probabilistic testing equivalence, in which success probabilities are compared in a trace-by-trace fashion rather than cumulatively.

Likewise, under memoryless schedulers, a different definition of probabilistic trace equivalence allows compositionality to be recovered without resorting to distributed scheduling. In the probabilistic trace-distribution equivalence of  [25], for each resolution of either process there must exist a resolution of the other process such that the two resolutions are fully matching, in the sense that, for every trace, both resolutions feature the same probability of executing that trace. We call it probabilistic trace post-equivalence as the quantification over traces occurs after the quantifications over resolutions. In  [3] it was proposed to exchange the order of those quantifications, which avoids hardly justifiable process distinctions and regains compositionality. Given an arbitrary trace, for each resolution of either process there must exist a resolution of the other process such that both of them exhibit the same probability of executing that trace. In this case, we speak of partially matching resolutions, as a resolution of either process can be matched by different resolutions of the other process with respect to different traces. We call the resulting relation probabilistic trace pre-equivalence, because the quantification over traces occurs before the quantifications over resolutions.

Congruence with respect to parallel composition, which is ensured by distributed scheduling, is not the only desirable property of probabilistic trace equivalences. In addition to compositionality with respect to other typical process operators, it is necessary to address inclusion of probabilistic bisimilarity  [27] as well as backward compatibility with trace equivalences over less expressive processes such as fully nondeterministic ones  [8] and fully probabilistic ones  [20]. As recently shown in  [2], the validity of all these properties critically depends on the capability of limiting the freedom of schedulers and can be achieved if we restrict ourselves to coherent resolutions of nondeterminism. Similar to  [14], the basic idea is that schedulers cannot select different continuations in states of a process that are equivalent to each other, so that also the states to which they correspond in any resolution of the process have equivalent continuations.

The focus of this paper is on alternative characterizazions of trace semantics. In a fully nondeterministic setting, two processes are trace equivalent iff, for each trace \(\alpha \), both processes can perform \(\alpha \) or neither can. An immediate alternative characterization is that two trace equivalent processes possess the same trace set  [8], where this set can be viewed as the language accepted by the automata underlying those processes. Likewise, two fully probabilistic processes are trace equivalent iff, for each trace \(\alpha \), both processes can perform \(\alpha \) with the same probability, which amounts to possessing the same set of traces each weighted with its execution probability  [20], i.e., the same probabilistic language. In either case, process equivalence reduces to (possibly weighted) trace set equality.

Straightforward characterizations of that form are not possible in the case of nondeterministic and probabilistic processes, because (i) traces can have different execution probabilities in different coherent resolutions and (ii) trace semantics can be defined according to different approaches leading to probabilistic trace post-/pre-equivalences. This motivates the investigation of alternative characterizations for the two aforementioned equivalences under coherent resolutions arising from centralized, memoryless schedulers – i.e., as they were defined in  [2] – which is the subject of this paper.

The construction developed in  [2] to formalize the coherency constraints relies on coherent trace distributions, i.e., suitable families of sets of traces weighted with their execution probabilities in a given resolution. Therefore, one may expect that the coherency-based variant of the probabilistic trace-distribution equivalence of  [25], i.e., probabilistic trace post-equivalence, can be characterized in terms of coherent trace distribution equality. We will show by means of an example that this is not the case. The characterization of the coherency-based variant of probabilistic trace post-equivalence relies on the equality of something stronger, which we will call fully coherent trace distributions and could also replace coherent trace distributions in the coherency constraints.

The coherency-based variant of the probabilistic trace pre-equivalence of  [3] is less discriminating because it treats traces individually without keeping track of the resolutions in which they can be executed. We will show that it can thus be characterized through the equality of something weaker than coherent trace distributions, which we will call coherent weighted trace sets and is constituted by suitable sets of traces weighted with their execution probabilities. We will also illustrate by means of an example that we cannot use them to set up adequate coherency constraints. In conclusion, fully coherent trace distributions, coherent trace distributions, and coherent weighted trace sets form a hierarchy in which every layer serves a different purpose.

This paper is organized as follows. In Sect. 2 we recall simple probabilistic automata and resolutions of nondeterminism, while in Sect. 3 we recall the two probabilistic trace equivalences together with three anomalies that can be avoided by resorting to coherent resolutions. In Sect. 4 we show some properties of coherent trace distributions and coherent resolutions, which are then exploited in Sects. 5 and 6 to develop the alternative characterizations of the coherency-based variants of the two equivalences, respectively relying on the equality of fully coherent trace distributions and on the equality of coherent weighted trace sets. Finally, in Sect. 7 we provide some concluding remarks.

2 Nondeterministic and Probabilistic Models

We formalize systems featuring nondeterminism and probabilities through a variant of simple probabilistic automata  [24], in which we do not distinguish between external and internal actions.

Definition 1

A nondeterministic and probabilistic labeled transition system, NPLTS for short, is a triple \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) where \(S \ne \emptyset \) is an at most countable set of states, \(A \ne \emptyset \) is a countable set of transition-labeling actions, and \( \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \! \subseteq S \times A \times \textit{Distr}(S)\) is a transition relation, with \(\textit{Distr}(S)\) being the set of discrete probability distributions over S.

A transition \((s, a, \varDelta )\) is written \(s \, {\mathop {\longrightarrow }\limits ^{a}}_{} \, \varDelta \). We say that \(s' \in S\) is not reachable from s via that a-transition if \(\varDelta (s') = 0\), otherwise we say that it is reachable with probability \(p = \varDelta (s')\). The reachable states form the support of the target distribution \(\varDelta \), i.e., \(\textit{supp}(\varDelta ) = \{ s' \in S \mid \varDelta (s') > 0 \}\). 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 different from 1 (see the forthcoming Figs. 1, 2, 3, 4 and 5).

An NPLTS represents (i) a fully nondeterministic process when every transition has a target distribution with a singleton support, (ii) a fully probabilistic process when every state has at most one outgoing transition, or (iii) a Markov decision process when for each action any state has at most one outgoing transition labeled with that action implying the absence of internal nondeterminism.

Definition 2

Let \(\mathcal {L}= (S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s, s' \in S\). We say that the finite sequence of steps:

figure b

is a computation of \(\mathcal {L}\) of length \(n \in \mathbb {N}\) from \(s = s_{0}\) to \(s' = s_{n}\) compatible with trace \(\alpha = a_{1} \, a_{2} \dots a_{n} \in A^{*}\), written \(c \in \mathcal {CC}(s, \alpha )\), iff for each step in c there is a transition \(s_{i - 1} \, {\mathop {\longrightarrow }\limits ^{a_{i}}}_{} \, \varDelta _{i}\) in \(\mathcal {L}\) such that \(s_{i} \in \textit{supp}(\varDelta _{i})\), \(1 \le i \le n\), where:

  • \(\varDelta _{i}(s_{i})\) is the execution probability of step conditioned on the selection of transition \(s_{i - 1} \, {\mathop {\longrightarrow }\limits ^{a_{i}}}_{} \, \varDelta _{i}\) at state \(s_{i - 1}\), or simply the execution probability of that step if \(\mathcal {L}\) is fully probabilistic.

  • \(\textit{prob}(c) = \prod _{1 \le i \le n} \varDelta _{i}(s_{i})\) is the execution probability of c if \(\mathcal {L}\) is fully probabilistic, assuming that \(\textit{prob}(c) = 1\) when \(n = 0\).

  • For \(C \subseteq \mathcal {CC}(s, \alpha )\), we let \(\textit{prob}(C) = \sum _{c \in C} \textit{prob}(c)\) if \(\mathcal {L}\) is fully probabilistic, provided that no computation in C is a proper prefix of one of the others.

When several transitions depart from the same state s of an NPLTS \(\mathcal {L}\), they describe a nondeterministic choice among different 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 \(\mathcal {Z}\) with a tree-like structure, whose branching points correspond to target distributions of transitions deriving from those of \(\mathcal {L}\).

Fig. 1.
figure 1

Lack of injectivity breaks structure preservation

Full size image

In  [2] we examined 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 structure-modifying approach (i) a transition can be produced by probabilistically combining transitions of the original model via a randomized scheduler  [24], or (ii) a state can be obtained by probabilistically splitting states of the original model via an interpolating scheduler  [12], or (iii) a combination thereof  [7].

As in  [2], 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  [5, 17] we introduce a correspondence function \(\textit{corr}_{\mathcal {Z}} : Z \rightarrow S\) from the acyclic state space of the resolution \(\mathcal {Z}= (Z, A, \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {Z}} \, \!)\) being built, to the possibly cyclic state space of the considered model \(\mathcal {L}= (S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {L}} \, \!)\). For each transition \(z \, {\mathop {\longrightarrow }\limits ^{a}}_{\mathcal {Z}} \, \varDelta \), the function \(\textit{corr}_{\mathcal {Z}}\) must preserve the probabilities of all the states corresponding to those in \(\textit{supp}(\varDelta )\) and must be injective over \(\textit{supp}(\varDelta )\). 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 exemplified in Fig. 1. The correspondence function that maps z to s, \(z'_{1}\) and \(z'_{2}\) to \(s'_{1}\), and \(z''_{1}\) and \(z''_{2}\) to \(s''_{1}\) 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.

Definition 3

Let \(\mathcal {L}= (S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {L}} \, \!)\) be an NPLTS and \(s \in S\). An acyclic NPLTS \(\mathcal {Z}= (Z, A, \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {Z}} \, \!)\) is a structure-preserving resolution of s, written \(\mathcal {Z}\in \textit{Res}_\mathrm{sp}(s)\), iff there exists a correspondence function \(\textit{corr}_{\mathcal {Z}} : Z \rightarrow S\) such that \(s = \textit{corr}_{\mathcal {Z}}(z_{s})\), for some \(z_{s} \in Z\) acting as the initial state of \(\mathcal {Z}\), and for all \(z \in Z\) it holds that:

  • If \(z \, {\mathop {\longrightarrow }\limits ^{a}}_{\mathcal {Z}} \, \varDelta \) then \(\textit{corr}_{\mathcal {Z}}(z) \, {\mathop {\longrightarrow }\limits ^{a}}_{\mathcal {L}} \, \varGamma \), with \(\textit{corr}_{\mathcal {Z}}\) being injective over \(\textit{supp}(\varDelta )\) and satisfying \(\varDelta (z') = \varGamma (\textit{corr}_{\mathcal {Z}}(z'))\) for all \(z' \in \textit{supp}(\varDelta )\).

  • At most one transition departs from z.

Fig. 2.
figure 2

\(\sim _\mathrm{PTr}^\mathrm{post}\) is strictly finer than \(\sim _\mathrm{PTr}^\mathrm{pre}\): \(s_{1} \not \sim _\mathrm{PTr}^\mathrm{post} s_{2} \not \sim _\mathrm{PTr}^\mathrm{post} s_{3}\), \(s_{1} \sim _\mathrm{PTr}^\mathrm{pre} s_{2} \sim _\mathrm{PTr}^\mathrm{pre} s_{3}\)

Full size image

3 Probabilistic Trace Equivalences and Their Anomalies

There is only one way of defining trace semantics for fully nondeterministic processes  [8] and for fully probabilistic processes  [20]. In contrast, this is not the case with processes featuring both nondeterminism and probabilities, as shown in the spectrum of behavioral equivalences for NPLTS models studied in  [4].

The first probabilistic trace equivalence that we consider is the one of  [25]. Two states are deemed equivalent when every resolution of either state is matched by a resolution of the other, in the sense that for each trace both resolutions execute that trace with the same probability. We call it probabilistic trace post-equivalence because the quantification over traces occurs after selecting the two fully matching resolutions as underlined in the definition below, where \(z_{s_{i}}\) denotes both the initial state of \(\mathcal {Z}_{i}\) and the state to which \(s_{i}\) corresponds.

Definition 4

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s_{1}, s_{2} \in S\). We let \(s_{1} \sim _\mathrm{PTr}^\mathrm{post} s_{2}\) iff for each \(\mathcal {Z}_{1} \in \textit{Res}_\mathrm{sp}(s_{1})\) there exists \(\mathcal {Z}_{2} \in \textit{Res}_\mathrm{sp}(s_{2})\) such that :

figure f

and also the condition obtained by exchanging \(\mathcal {Z}_{1}\) with \(\mathcal {Z}_{2}\) is satisfied.

The second probabilistic trace equivalence is the one of  [3], which is a congruence with respect to parallel composition. It is less restrictive than the previous equivalence because, given two states, a resolution of either state can be matched by different resolutions of the other with respect to different traces. We call it probabilistic trace pre-equivalence because traces are fixed before selecting the two partially matching resolutions.

Definition 5

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s_{1}, s_{2} \in S\). We let \(s_{1} \sim _\mathrm{PTr}^\mathrm{pre} s_{2}\) iff, , for each \(\mathcal {Z}_{1} \in \textit{Res}_\mathrm{sp}(s_{1})\) there is \(\mathcal {Z}_{2} \in \textit{Res}_\mathrm{sp}(s_{2})\) such that:

figure i

and also the condition obtained by exchanging \(\mathcal {Z}_{1}\) with \(\mathcal {Z}_{2}\) is satisfied.

In Fig. 2 we show three NPLTS models whose initial states \(s_{1}\), \(s_{2}\), \(s_{3}\) are pairwise distinguished by \(\sim _\mathrm{PTr}^\mathrm{post}\) but identified by \(\sim _\mathrm{PTr}^\mathrm{pre}\), because for all \(i = 1, \dots , 4\) the probability of executing trace \(a \, b_{i}\) is the same in the three models.

Although deterministic schedulers are very intuitive, the rigid preservation they ensure about the structure of the original model, together with their freedom of performing choices inconsistent with each other in states with equivalent continuations, causes the two considered probabilistic trace equivalences to be overdiscriminating. This results in the violation of a number of desirable properties (a fact that also happens with structure-modifying schedulers, but to a much lesser extent). More precisely, in  [2] we showed that \(\sim _\mathrm{PTr}^\mathrm{post}\) and \(\sim _\mathrm{PTr}^\mathrm{pre}\):

  • are not coarser than probabilistic bisimilarity under deterministic schedulers;

  • are not congruences w.r.t. action prefix under deterministic schedulers;

  • are not compatible with their version for fully probabilistic processes.

Fig. 3.
figure 3

Three anomalies of the probabilistic trace equivalences \(\sim _\mathrm{PTr}^\mathrm{post}\) and \(\sim _\mathrm{PTr}^\mathrm{pre}\)

Full size image

The first anomaly is illustrated by the two NPLTS models in Fig. 3 whose initial states are \(s_{1}\) and \(s_{2}\). They are probabilistic bisimilar in the sense of  [27] but \(s_{1} \not \sim _\mathrm{PTr}^\mathrm{post} s_{2}\) and \(s_{1} \not \sim _\mathrm{PTr}^\mathrm{pre} s_{2}\) because of the resolution whose initial state is \(z_{2}\), where trace \(a \, b\) is executable with probability p instead of 1. This resolution belongs to \(\textit{Res}_\mathrm{sp}(s_{2}) \setminus \textit{Res}_\mathrm{sp}(s_{1})\) as it does not preserve the structure of the NPLTS whose initial state is \(s_{1}\). Therefore, the two probabilistic trace equivalences do not include probabilistic bisimilarity.

The second anomaly is illustrated by the two NPLTS models in Fig. 3 whose initial states are \(s_{3}\) and \(s_{4}\). After the two a-transitions, two distributions are reached that are probabilistic trace equivalent, in the sense that for each class of equivalent states they both assign the same probability to that class. However, it holds that \(s_{3} \not \sim _\mathrm{PTr}^\mathrm{post} s_{4}\) and \(s_{3} \not \sim _\mathrm{PTr}^\mathrm{pre} s_{4}\) due to the resolution whose initial state is \(z_{3}\), where trace \(a \, a' \, b\) is executable with probability p instead of 1. This resolution belongs to \(\textit{Res}_\mathrm{sp}(s_{3}) \setminus \textit{Res}_\mathrm{sp}(s_{4})\) as it does not preserve the structure of the NPLTS whose initial state is \(s_{4}\). Therefore, the two probabilistic trace equivalences are not congruences with respect to the action prefix operator, which concatenates the execution of an action with a process distribution.

The third anomaly is illustrated by the two NPLTS models in Fig. 3 whose initial states are \(s_{5}\) and \(s_{6}\). They are identified by the trace equivalence for fully probabilistic processes of  [20], which does not use schedulers at all as in those processes there are no nondeterministic choices to be solved. However, it turns out that \(s_{5} \not \sim _\mathrm{PTr}^\mathrm{post} s_{6}\) and \(s_{5} \not \sim _\mathrm{PTr}^\mathrm{pre} s_{6}\) because \(\sim _\mathrm{PTr}^\mathrm{post}\) and \(\sim _\mathrm{PTr}^\mathrm{pre}\) do make use of schedulers, and schedulers may decide of stopping the execution. This is witnessed by the resolution whose initial state is \(z_{6}\) – notice that the scheduler has decided to stop the execution at \(z''_{6}\) – where not only trace \(a \, b \, c_{1}\) but also trace \(a \, b\) is executable with probability p. This resolution belongs to \(\textit{Res}_\mathrm{sp}(s_{6}) \setminus \textit{Res}_\mathrm{sp}(s_{5})\) as it does not preserve the structure of the NPLTS whose initial state is \(s_{5}\). Therefore, the two probabilistic trace equivalences are not backward compatible with the one for fully probabilistic processes.

4 Properties of Coherency

The anomalies shown in Fig. 3 are due to the freedom of schedulers of making different decisions in states enabling the same actions. In  [2] 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 as well.

The coherency constraints implementing this idea have been expressed in  [2] by reasoning on coherent trace distributions, i.e., families of sets of traces weighted with their execution probabilities in a given resolution, built through the following operations.

Definition 6

Let \(A \ne \emptyset \) be a countable set. For \(a \in A\), \(p \in \mathbb {R}\), \(\textit{TD}\subseteq 2^{A^{*} \times \mathbb {R}}\), and \(T \subseteq A^{*} \times \mathbb {R}\) we define:

figure k

Weighted trace set addition \(T_{1} + T_{2}\) is commutative and associative, with probabilities of identical 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 \(\textit{TD}_{1} + \textit{TD}_{2}\) 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 \(T_{1} \in \textit{TD}_{1}\) is summed with every weighted trace set \(T_{2} \in \textit{TD}_{2}\) – so to characterize an overall resolution – unless \(\textit{TD}_{1}\) and \(\textit{TD}_{2}\) have the same family of trace sets, in which case summation is restricted to weighted trace sets featuring the same traces for the sake of coherency. Due to the lack of associativity, in the definition below all trace distributions \(\varDelta (s') \cdot \textit{TD}_{n - 1}^\mathrm{c}(s')\) exhibiting the same family \(\varTheta \) of trace sets have to be summed up first, which is ensured by the presence of a double summation.

Definition 7

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s \in S\). The coherent trace distribution of s is the subset of \(2^{A^{*} \times \mathbb {R}_{]0, 1]}}\) defined as follows:

\(\textit{TD}^\mathrm{c}(s) \, = \, \bigcup _{n \in \mathbb {N}} \textit{TD}_{n}^\mathrm{c}(s)\)

with the coherent trace distribution of s whose traces have length at most n being defined as:

\(\textit{TD}_{n}^\mathrm{c}(s) \, = \, \left\{ \begin{array}{ll} (\varepsilon , 1) \dagger \bigcup \limits _{s \, {\mathop {\longrightarrow }\limits ^{a}}_{} \, \varDelta } a \, . \left( \sum \limits _{\varTheta \in \textit{tr}(\varDelta , n - 1)} \, \sum \limits _{s' \in \textit{supp}(\varDelta )}^{\textit{tr}(\textit{TD}_{n - 1}^\mathrm{c}(s')) = \varTheta } \varDelta (s') \cdot \textit{TD}_{n - 1}^\mathrm{c}(s') \right) \\ &{} \text {if n > 0 and { s} has outgoing transitions} \\ \{ \{ (\varepsilon , 1) \} \} \\ &{} \text {otherwise} \\ \end{array} \right. \)

where \(\textit{tr}(\varDelta , n - 1) = \{ \textit{tr}(\textit{TD}_{n - 1}^\mathrm{c}(s')) \mid s' \in \textit{supp}(\varDelta ) \}\) and the operator \((\varepsilon , 1) \dagger \_\) is such that \((\varepsilon , 1) \dagger \textit{TD}\, = \, \{ \{ (\varepsilon , 1) \} \cup T \mid T \in \textit{TD}\}\).

In the case of a fully probabilistic NPLTS, due to the absence of nondeterminism any coherent trace distribution \(\textit{TD}_{n}^\mathrm{c}(s)\) contains a single weighted trace set. This holds in particular for resolutions.

Proposition 1

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be a fully probabilistic NPLTS, \(s \in S\), \(n \in \mathbb {N}\). Let \(A^{\le n} = \{ \alpha \in A^{*} \mid |\alpha | \le n \}\). Then \(\textit{TD}_{n}^\mathrm{c}(s) = \{ \{ (\alpha , p) \in A^{\le n} \times \mathbb {R}_{]0, 1]} \mid \textit{prob}(\mathcal {CC}(s, \alpha )) = p \} \}\).

As for the relationship between \(\textit{TD}_{n}^\mathrm{c}(s)\) and \(\textit{TD}_{n - 1}^\mathrm{c}(s)\), it turns out that every element of the former contains the same traces as an element of the latter. As we will see in the next section, their probabilities may differ.

Proposition 2

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS, \(s \in S\), \(n \in \mathbb {N}_{\ge 1}\). Then for all \(T \in \textit{TD}_{n}^\mathrm{c}(s)\) there exists \(T' \in \textit{TD}_{n - 1}^\mathrm{c}(s)\) such that \(\textit{tr}(T') \subseteq \textit{tr}(T)\).

For the NPLTS models in Fig. 3 we have that:

  • \(\textit{TD}^\mathrm{c}(s'_{2}) = \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (b, 1) \}, \{ (\varepsilon , 1), (c, 1) \} \} = \textit{TD}^\mathrm{c}(s''_{2})\) while in the related resolution states it holds that \(\textit{TD}^\mathrm{c}(z'_{2}) = \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (b, 1) \} \} \ne \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (c, 1) \} \} = \textit{TD}^\mathrm{c}(z''_{2})\).

  • \(\textit{TD}^\mathrm{c}(s'_{3}) = \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (a', 1) \}, \{ (\varepsilon , 1), (a', 1), (a' \, b, 1) \}, \{ (\varepsilon , 1), (a', 1), (a' \, c, 1) \} \} = \textit{TD}^\mathrm{c}(s''_{3})\) but \(\textit{TD}^\mathrm{c}(z'_{3}) = \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (a', 1) \}, \{ (\varepsilon , 1), (a', 1), (a' \, b, 1) \} \} \ne \{ \{ (\varepsilon , 1) \}, \{ (\varepsilon , 1), (a', 1) \}, \{ (\varepsilon , 1), (a', 1), (a' \, c, 1) \} \} = \textit{TD}^\mathrm{c}(z''_{3})\).

  • \(\textit{TD}_{1}^\mathrm{c}(s'_{6}) = \{ \{ (\varepsilon , 1), (b, 1) \} \} = \textit{TD}_{1}^\mathrm{c}(s''_{6})\) but \(\textit{TD}_{1}^\mathrm{c}(z'_{6}) = \{ \{ (\varepsilon , 1), (b, 1) \} \} \ne \{ \{ (\varepsilon , 1) \} \} = \textit{TD}_{1}^\mathrm{c}(z''_{6})\), which indicates that separate coherency constraints are needed relying on \(\textit{TD}_{n}^\mathrm{c}\) sets for every \(n \in \mathbb {N}\).

Further examples in  [2] show that the coherency constraints should be based on \(\textit{TD}_{n}^\mathrm{c}\) sets up to the probabilities they contain, i.e., the constraints should rely on \(\textit{tr}(\textit{TD}_{n}^\mathrm{c})\) sets. Moreover, for every \(n \in \mathbb {N}\), those examples call for a complete presence in each resolution of computations of length n if any, including possible shorter maximal computations. Note that trace completeness up to length n is looser than requiring resolution maximality.

Definition 8

Let \(\mathcal {L}= (S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {L}} \, \!)\) be an NPLTS, \(s \in S\), and \(\mathcal {Z}= (Z, A, \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {Z}} \, \!) \in \textit{Res}_\mathrm{sp}(s)\) with correspondence function \(\textit{corr}_{\mathcal {Z}} : Z \rightarrow S\). We say that \(\mathcal {Z}\) is a coherent resolution of s, written \(\mathcal {Z}\in \textit{Res}_\mathrm{sp}^\mathrm{c}(s)\), iff for all \(z \in Z\), whenever \(z \, {\mathop {\longrightarrow }\limits ^{a}}_{\mathcal {Z}} \, \varDelta \), then for all \(n \in \mathbb {N}\):

  1. 1.

    \(\textit{tr}(\textit{TD}_{n}^\mathrm{c}(\textit{corr}_{\mathcal {Z}}(z'))) \! = \! \textit{tr}(\textit{TD}_{n}^\mathrm{c}(\textit{corr}_{\mathcal {Z}}(z''))) \Longrightarrow \textit{tr}(\textit{TD}_{n}^\mathrm{c}(z')) \! = \! \textit{tr}(\textit{TD}_{n}^\mathrm{c}(z''))\) for all \(z', z'' \in \textit{supp}(\varDelta )\).

  2. 2.

    For all \(z' \in \textit{supp}(\varDelta )\), the only \(T \in \textit{TD}_{n}^\mathrm{c}(z')\) admits \(\bar{T} \in \textit{TD}_{n}^\mathrm{c}(\textit{corr}_{\mathcal {Z}}(z'))\) such that \(\textit{tr}(T) = \textit{tr}(\bar{T})\).

Any complete submodel rooted at a state z of a coherent resolution turns out to be coherent too, where complete means that no state reachable from z in the resolution is cut off in the resolution submodel. Completeness is important for satisfying in particular the second coherency constraint of Definition 8.

Proposition 3

Let \(\mathcal {L}= (S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {L}} \, \!)\) be an NPLTS, \(s \in S\), \(\mathcal {Z}= (Z, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {Z}} \, \!) \in \textit{Res}_\mathrm{sp}^\mathrm{c}(s)\) with correspondence function \(\textit{corr}_{\mathcal {Z}} : Z \rightarrow S\). Let \(\mathcal {Z}'_{z} = (Z', A, \, {\mathop {\longrightarrow }\limits ^{}}_{\mathcal {Z}'} \, \!)\) be the complete submodel of \(\mathcal {Z}\) rooted at \(z \in Z\). Then \(\mathcal {Z}'_{z} \in \textit{Res}_\mathrm{sp}^\mathrm{c}(\textit{corr}_{\mathcal {Z}}(z))\).

The resolutions in Fig. 3 do not respectively belong to \(\textit{Res}_\mathrm{sp}^\mathrm{c}(s_{2})\), \(\textit{Res}_\mathrm{sp}^\mathrm{c}(s_{3})\), \(\textit{Res}_\mathrm{sp}^\mathrm{c}(s_{6})\). We proved in Thm. 1 of  [2] that the examined anomalies disappear by substituting \(\textit{Res}_\mathrm{sp}^\mathrm{c}\) for \(\textit{Res}_\mathrm{sp}\) in Definitions 4 and 5. This replacement yields the two coherency-based probabilistic trace equivalences \(\sim _\mathrm{PTr}^\mathrm{post, c}\) and \(\sim _\mathrm{PTr}^\mathrm{pre, c}\) for which we will investigate alternative characterizations in the next two sections by exploiting the properties shown in Propositions 1, 2, and 3.

5 Alternative Characterization of \(\sim _\mathrm{PTr}^\mathrm{post, c}\)

The definition of \(\sim _\mathrm{PTr}^\mathrm{post, c}\) essentially requires that two states have the same trace distributions. Therefore, it is natural to expect an alternative characterization of \(\sim _\mathrm{PTr}^\mathrm{post, c}\) based on the construction of Definition 7. Incidentally, this would fully justify the construction itself, given that the probabilities contained in the \(\textit{TD}_{n}^\mathrm{c}\) sets have not been exploited in the coherency constraints of Definition 8. However, for an NPLTS \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) and \(s \in S\), the set \(\textit{TD}^\mathrm{c}(s)\) may contain weighted traces that break coherency, hence that set cannot be used for characterization purposes.

For example, consider the NPLTS in Fig. 4. We have that:

$$ {\textit{TD}_{1}^\mathrm{c}(s_{1}) \, = \, \{ \{ (\varepsilon , 1), (b, 1) \} \} \, = \, \textit{TD}_{1}^\mathrm{c}(s_{2})}$$

and also:

$$ {\textit{TD}_{2}^\mathrm{c}(s_{1}) \, = \, \{ \{ (\varepsilon , 1), (b, 1), (b \, c, 1) \}, \{ (\varepsilon , 1), (b, 1), (b \, d, 1) \} \} \, = \, \textit{TD}_{2}^\mathrm{c}(s_{2})} $$

because in the complete submodel rooted at \(s_{1}\) it holds that:

\(\textit{TD}_{1}^\mathrm{c}(s'_{1}) \, = \, \{ \{ (\varepsilon , 1), (c, 1) \}, \{ (\varepsilon , 1), (d, 1) \} \} \, = \, \textit{TD}_{1}^\mathrm{c}(s''_{1})\)

and hence, when applying Definition 7 to compute \(\textit{TD}_{2}^\mathrm{c}(s_{1})\), according to Definition 6 the summation is restricted to weighted trace sets featuring the same traces as:

\(\textit{tr}(\textit{TD}_{1}^\mathrm{c}(s'_{1})) \, = \, \{ \{ \varepsilon , c \}, \{ \varepsilon , d \} \} \, = \, \textit{tr}(\textit{TD}_{1}^\mathrm{c}(s''_{1}))\)

Nevertheless, since:

\(\begin{array}{rcl} \textit{TD}_{2}^\mathrm{c}(s'_{1}) &{} \, = \, &{} \{ \{ (\varepsilon , 1), (c, 1), (c \, e_{1}, 1) \}, \{ (\varepsilon , 1), (d, 1), (d \, e_{2}, 1) \} \} \\ \textit{TD}_{2}^\mathrm{c}(s''_{1}) &{} = &{} \{ \{ (\varepsilon , 1), (c, 1), (c \, e_{3}, 1) \}, \{ (\varepsilon , 1), (d, 1), (d \, e_{4}, 1) \} \} \\ \end{array}\)

where:

\(\textit{tr}(\textit{TD}_{2}^\mathrm{c}(s'_{1})) = \{ \{ \varepsilon , c, c \, e_{1} \}, \! \{ \varepsilon , d, d \, e_{2} \} \} \ne \{ \{ \varepsilon , c, c \, e_{3} \}, \! \{ \varepsilon , d, d \, e_{4} \} \} = \textit{tr}(\textit{TD}_{2}^\mathrm{c}(s''_{1}))\)

we subsequently derive that:

\(\begin{array}{rcl} \textit{TD}_{3}^\mathrm{c}(s_{1}) &{} \, = \, &{} (\varepsilon , 1) \; \dagger \\ &{} &{} (\{ \{ (b, p), (b \, c, p), (b \, c \, e_{1}, p) \}, \\ &{} &{} \,\,\,\, \{ (b, p), (b \, d, p), (b \, d \, e_{2}, p) \} \} \; + \\ &{} &{} \,\, \{ \{ (b, 1 - p), (b \, c, 1 - p), (b \, c \, e_{3}, 1 - p) \}, \\ &{} &{} \,\,\,\, \{ (b, 1 - p), (b \, d, 1 - p), (b \, d \, e_{4}, 1 - p) \} \}) \\ &{} = &{} \{ \{ (\varepsilon , 1), (b, 1), (b \, c, 1), (b \, c \, e_{1}, p), (b \, c \, e_{3}, 1 - p) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (b, 1), (b \, c, p), (b \, d, 1 - p), (b \, c \, e_{1}, p), (b \, d \, e_{4}, 1 - p) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (b, 1), (b \, d, p), (b \, c, 1 - p), (b \, d \, e_{2}, p), (b \, c \, e_{3}, 1 - p) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (b, 1), (b \, d, 1), (b \, d \, e_{2}, p), (b \, d \, e_{4}, 1 - p) \} \} \\ \end{array}\)

whereas:

\(\begin{array}{rcl} \textit{TD}_{3}^\mathrm{c}(s_{2}) &{} \, = \, &{} \{ \{ (\varepsilon , 1), (b, 1), (b \, c, 1), (b \, c \, e_{1}, p), (b \, c \, e_{3}, 1 - p) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (b, 1), (b \, d, 1), (b \, d \, e_{2}, p), (b \, d \, e_{4}, 1 - p) \} \} \\ \end{array}\)

Therefore, in the calculation of \(\textit{TD}_{4}^\mathrm{c}(s)\) we cannot simply sum up weighted trace sets in \(\textit{TD}_{3}^\mathrm{c}(s_{1})\) and in \(\textit{TD}_{3}^\mathrm{c}(s_{2})\) that exhibit the same traces. This is due to the presence in \(\textit{TD}_{3}^\mathrm{c}(s_{1})\) of the following two weighted trace sets:

\(\begin{array}{l} \{ (\varepsilon , 1), (b, 1), (b \, c, p), (b \, d, 1 - p), (b \, c \, e_{1}, p), (b \, d \, e_{4}, 1 - p) \} \\ \{ (\varepsilon , 1), (b, 1), (b \, d, p), (b \, c, 1 - p), (b \, d \, e_{2}, p), (b \, c \, e_{3}, 1 - p) \} \\ \end{array}\)

which cannot be exposed by any coherent resolution. The key observation is that coherency constraints on traces like \(b \, c\) and \(b \, d\) are ignored, hence those two weighted trace sets in \(\textit{TD}_{3}^\mathrm{c}(s_{1})\) are not extensions of weighted trace sets in \(\textit{TD}_{2}^\mathrm{c}(s_{1})\). Indeed, neither of those weighted trace sets in \(\textit{TD}_{3}^\mathrm{c}(s_{1})\) includes as a subset a weighted trace set in \(\textit{TD}_{2}^\mathrm{c}(s_{1})\) because of the different probabilities of the aforementioned traces in the considered sets (see the sentence before Proposition 2).

Fig. 4.
figure 4

Full coherency is necessary to reconcile \(\textit{TD}_{3}^\mathrm{c}(s_{1})\) and \(\textit{TD}_{3}^\mathrm{c}(s_{2})\)

Full size image

This example reveals that the construction of Definition 7, together with weighted trace set addition and trace distribution addition as provided in Definition 6, are appropriate to set up the coherency constraints in Definition 8, but not to characterize the trace distributions of coherent resolutions. To achieve this, every set \(\textit{TD}_{n}^\mathrm{c}(s)\), with \(n > 0\) and s having outgoing transitions, should incrementally build on \(\textit{TD}_{n - 1}^\mathrm{c}(s)\), in the sense that every weighted trace set in the former should include as a subset a weighted trace set in the latter (a monotonicity-like property stronger than the one of Proposition 2). We thus introduce a variant of coherent trace distribution, which we call fully coherent trace distribution.

Definition 9

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s \in S\). The fully coherent trace distribution of s is the subset of \(2^{A^{*} \times \mathbb {R}_{]0, 1]}}\) defined as follows:

\(\textit{TD}^\mathrm{fc}(s) \, = \, \bigcup _{n \in \mathbb {N}} \textit{TD}_{n}^\mathrm{fc}(s)\)

with the fully coherent trace distribution of s whose traces have length at most n being the subset of \(\textit{TD}_{n}^\mathrm{c}(s)\) defined as:

figure r

For the NPLTS in Fig. 4 we have that:

\(\begin{array}{rcccl} \textit{TD}_{3}^\mathrm{fc}(s_{1}) &{} \, = \! &{} \{ \{ (\varepsilon , 1), (b, 1), (b \, c, 1), (b \, c \, e_{1}, p), (b \, c \, e_{3}, 1 - p) \}, &{} &{} \\ &{} &{} \,\,\,\, \{ (\varepsilon , 1), (b, 1), (b \, d, 1), (b \, d \, e_{2}, p), (b \, d \, e_{4}, 1 - p) \} \} &{} \, = \, &{} \textit{TD}_{3}^\mathrm{fc}(s_{2}) \\ \end{array}\)

and overall \(\textit{TD}^\mathrm{fc}(s) \, = \, \bigcup _{0 \le n \le 4} \textit{TD}_{n}^\mathrm{fc}(s)\) where:

\(\begin{array}{rcl} \textit{TD}_{0}^\mathrm{fc}(s) &{} \, = \, &{} \{ \{ (\varepsilon , 1) \} \} \\ \textit{TD}_{1}^\mathrm{fc}(s) &{} = &{} \{ \{ (\varepsilon , 1), (a, 1) \} \} \\ \textit{TD}_{2}^\mathrm{fc}(s) &{} = &{} \{ \{ (\varepsilon , 1), (a, 1), (a \, b, 1) \} \} \\ \textit{TD}_{3}^\mathrm{fc}(s) &{} = &{} \{ \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, c, 1) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, d, 1) \} \} \\ \textit{TD}_{4}^\mathrm{fc}(s) &{} = &{} \{ \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, c, 1), (a \, b \, c \, e_{1}, p), (a \, b \, c \, e_{3}, 1 - p) \}, \\ &{} &{} \,\, \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, d, 1), (a \, b \, d \, e_{2}, p), (a \, b \, d \, e_{4}, 1 - p) \} \} \\ \end{array}\)

with the various sets \(\textit{TD}_{n}^\mathrm{fc}(s)\) precisely capturing the trace distributions of the coherent resolutions of s.

Fully coherent trace distributions \(\textit{TD}_{n}^\mathrm{fc}(s)\) coincide with coherent ones \(\textit{TD}_{n}^\mathrm{c}(s)\) when \(n \le 2\) as a consequence of Definition 6. The example in Fig. 4 shows that, when \(n \ge 3\), in general \(\textit{TD}_{n}^\mathrm{fc}(s)\) cannot be recursively characterized as \(\textit{TD}_{n}^\mathrm{c}(s)\) in Definition 7 even though each element of a fully coherent trace distribution can be expressed as a sum of elements of other fully coherent trace distributions.

Proposition 4

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS, \(s \in S\), \(n \in \mathbb {N}\). If \(n \le 2\) or s has no outgoing transitions, then \(\textit{TD}_{n}^\mathrm{fc}(s) = \textit{TD}_{n}^\mathrm{c}(s)\), otherwise each element of \(\textit{TD}_{n}^\mathrm{fc}(s)\) is anyhow obtained by summing up a suitable element of \(\textit{TD}_{n - 1}^\mathrm{fc}(s')\) for every \(s'\) in the support of the target distribution of a transition of s.

By virtue of Proposition 1, the equality \(\textit{TD}_{n}^\mathrm{fc}(s) = \textit{TD}_{n}^\mathrm{c}(s)\) extends to all \(n \in \mathbb {N}\), i.e., fully coherent trace distributions boil down to coherent ones, in the case of a fully probabilistic NPLTS. This holds in particular for resolutions.

Proposition 5

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be a fully probabilistic NPLTS, \(s \in S\), \(n \in \mathbb {N}\). Then \(\textit{TD}_{n}^\mathrm{fc}(s) = \textit{TD}_{n}^\mathrm{c}(s)\).

Before presenting the characterization result, we need to revisit the coherency constraints of Definition 8 in the light of the example of Fig. 4. Suppose that each of the two terminal states reached by an \(e_{1}\)-transition is replaced by a distribution with two states in its target, reached with probabilities r and \(1 - r\) and both featuring a nondeterministic choice between an f-transition to a terminal state and a g-transition to a terminal state. According to Definition 8, after the leftmost \(e_{1}\)-transition either both f-transitions are selected or both g-transitions are selected, and the same holds after the rightmost \(e_{1}\)-transition.

However, from \(\textit{TD}_{3}^\mathrm{c}(s_{1}) \ne \textit{TD}_{3}^\mathrm{c}(s_{2})\) it follows that \(\textit{TD}_{4}^\mathrm{c}(s_{1}) \ne \textit{TD}_{4}^\mathrm{c}(s_{2})\), so that on \(s_{1}\) side both f-transitions may be selected while on \(s_{2}\) side both g-transitions may be selected instead, or vice versa. If we consider an NPLTS whose initial state \(s'\) has a single outgoing transition, which is labeled with a and reaches a model isomorphic to the complete submodel rooted at \(s_{2}\) in Fig. 4 (and extended in the aforementioned way after its only \(e_{1}\)-transition), \(s'\) would be distinguished from s instead of being identified with it. The coherency constraints of Definition 8 thus need to be strengthened by substituting \(\textit{TD}_{n}^\mathrm{fc}\) for \(\textit{TD}_{n}^\mathrm{c}\), in which case Thm. 1 of  [2] is still valid and \(\sim _\mathrm{PTr}^\mathrm{post, c}\) and \(\sim _\mathrm{PTr}^\mathrm{pre, c}\) are modified accordingly.

The following lemma, where Proposition 1 is exploited again together with Propositions 3, 4, and 5, lays the basis for a characterization of \(\sim _\mathrm{PTr}^\mathrm{post, c}\) in terms of fully coherent trace distribution equality. In the lemma, \(z_{s}\) denotes both the initial state of \(\mathcal {Z}\) and the state to which s corresponds.

Lemma 1

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS, \(s \in S\), \(n \in \mathbb {N}\), and \(T \subseteq A^{*} \times \mathbb {R}_{]0, 1]}\). Then \(T \in \textit{TD}_{n}^\mathrm{fc}(s)\) iff there exists \(\mathcal {Z}\in \textit{Res}_\mathrm{sp}^\mathrm{c}(s)\) such that \(\textit{TD}_{n}^\mathrm{fc}(z_{s}) = \{ T \}\).

Theorem 1

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s_{1}, s_{2} \in S\). Then \(s_{1} \sim _\mathrm{PTr}^\mathrm{post, c} s_{2}\) iff \(\textit{TD}^\mathrm{fc}(s_{1}) = \textit{TD}^\mathrm{fc}(s_{2})\).

6 Alternative Characterization of \(\sim _\mathrm{PTr}^\mathrm{pre, c}\)

As far as \(\sim _\mathrm{PTr}^\mathrm{pre, c}\) is concerned, similar to  [3] we can provide an alternative characterization based on sets \(T^\mathrm{c}(s)\) built by considering all weighted traces executable from state s at once, i.e., without keeping track of the resolutions of s in which they are feasible. This is consistent with the focus of \(\sim _\mathrm{PTr}^\mathrm{pre, c}\) on individual traces rather than on trace distributions. In the definition below, the double summation used in Definition 7 in the case that \(n > 0\) and s has outgoing transitions is not needed thanks to the commutativity and associativity of weighted trace set addition deriving from Definition 6.

Definition 10

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s \in S\). The coherent weighted trace set of s is the subset of \(A^{*} \times \mathbb {R}_{]0, 1]}\) defined as follows:

\(T^\mathrm{c}(s) \, = \, \bigcup _{n \in \mathbb {N}} T_{n}^\mathrm{c}(s)\)

with the coherent weighted trace set of s whose traces have length at most n being defined as:

\(T_{n}^\mathrm{c}(s) \, = \, \left\{ \begin{array}{ll} \{ (\varepsilon , 1) \} \cup \bigcup \limits _{s \, {\mathop {\longrightarrow }\limits ^{a}}_{} \, \varDelta } a \, . \left( \sum \limits _{s' \in \textit{supp}(\varDelta )} \varDelta (s') \cdot T_{n - 1}^\mathrm{c}(s') \right) \\ &{} \text {if n > 0 and { s} has outgoing transitions} \\ \{ (\varepsilon , 1) \} \\ &{} \text {otherwise} \\ \end{array} \right. \)

For the NPLTS in Fig. 4 we have that \(T^\mathrm{c}(s) \, = \, \bigcup _{0 \le n \le 4} T_{n}^\mathrm{c}(s)\) where:

\(\begin{array}{rcl} T_{0}^\mathrm{c}(s) &{} \, = \, &{} \{ (\varepsilon , 1) \} \\ T_{1}^\mathrm{c}(s) &{} = &{} \{ (\varepsilon , 1), (a, 1) \} \\ T_{2}^\mathrm{c}(s) &{} = &{} \{ (\varepsilon , 1), (a, 1), (a \, b, 1) \} \\ T_{3}^\mathrm{c}(s) &{} = &{} \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, c, 1), (a \, b \, d, 1) \} \\ T_{4}^\mathrm{c}(s) &{} = &{} \{ (\varepsilon , 1), (a, 1), (a \, b, 1), (a \, b \, c, 1), (a \, b \, d, 1), \\ &{} &{} \,\, (a \, b \, c \, e_{1}, p), (a \, b \, c \, e_{3}, 1 - p), (a \, b \, d \, e_{2}, p), (a \, b \, d \, e_{4}, 1 - p) \} \\ \end{array}\)

with the various sets \(T_{n}^\mathrm{c}(s)\) precisely capturing the weighted traces of the coherent resolutions of s.

It is easy to characterize \(T_{n}^\mathrm{c}(s)\) in the case of a fully probabilistic NPLTS. This holds in particular for resolutions.

Proposition 6

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be a fully probabilistic NPLTS, \(s \in S\), \(n \in \mathbb {N}\). Let \(A^{\le n} = \{ \alpha \in A^{*} \mid |\alpha | \le n \}\). Then \(T_{n}^\mathrm{c}(s) = \{ (\alpha , p) \in A^{\le n} \times \mathbb {R}_{]0, 1]} \mid \textit{prob}(\mathcal {CC}(s, \alpha )) = p \}\).

The construction in Definition 10 turns out to be monotonic, in the sense that \(T_{n}^\mathrm{c}(s)\) includes as a subset \(T_{n - 1}^\mathrm{c}(s)\).

Proposition 7

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS, \(s \in S\), \((\alpha , p) \in A^{*} \times \mathbb {R}_{]0, 1]}\), and \(n \in \mathbb {N}_{\ge |\alpha |}\). Then \((\alpha , p) \in T_{n}^\mathrm{c}(s)\) implies \((\alpha , p) \in T_{n + 1}^\mathrm{c}(s)\).

The following lemma, which exploits Proposition 6 and 7, provides the basis for a characterization of \(\sim _\mathrm{PTr}^\mathrm{pre, c}\) in terms of coherent weighted trace set equality. In the lemma, \(z_{s}\) denotes both the initial state of \(\mathcal {Z}\) and the state to which s corresponds.

Lemma 2

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS, \(s \in S\), and \((\alpha , p) \in A^{*} \times \mathbb {R}_{]0, 1]}\). Then \((\alpha , p) \in T^\mathrm{c}(s)\) iff there exists \(\mathcal {Z}\in \textit{Res}_\mathrm{sp}^\mathrm{c}(s)\) such that \(\textit{prob}(\mathcal {CC}(z_{s}, \alpha )) = p\).

Theorem 2

Let \((S, A, \! \, {\mathop {\longrightarrow }\limits ^{}}_{} \, \!)\) be an NPLTS and \(s_{1}, s_{2} \in S\). Then \(s_{1} \sim _\mathrm{PTr}^\mathrm{pre, c} s_{2}\) iff \(T^\mathrm{c}(s_{1}) = T^\mathrm{c}(s_{2})\).

We conclude with two remarks. The first one is that the construction in Definition 10 is identical to the one in Definition 3.5 of  [3], but this should not be the case as coherency was neglected in  [3]. Indeed, before Definition 3.5 of  [3] the definition of \(X + Y\) – i.e., \(T_{1} + T_{2}\) using the notation of this paper – should have included also \((\alpha , q_{1}) \in X\) and \((\alpha , q_{2}) \in Y\) without summing them up, otherwise the right-to-left implication in Lemma 3.7 of  [3] does not hold as can be seen from trace \(a \, b\) of the (incoherent) resolution in Fig. 3 of this paper whose initial state is \(z_{2}\). That definition of \(X + Y\) works here instead because the focus on coherency requires to always sum up the probabilities of weighted traces sharing the same trace.

The second remark is that looser coherency constraints, based on weighted trace sets rather than on trace distributions as in Definition 8, would not work. As anticipated in  [2], if we used \(T_{n}^\mathrm{c}\) sets instead of \(\textit{TD}_{n}^\mathrm{c}\) sets, then probabilistic trace equivalent NPLTS models like the ones in Fig. 5 would be told apart. Indeed, we would have \(\textit{tr}(T^\mathrm{c}(s'_{1})) = \{ \epsilon , b, b \, c_{1}, b \, c_{2}, b \, c \} = \textit{tr}(T^\mathrm{c}(s'_{2}))\) – whereas \(\textit{tr}(\textit{TD}^\mathrm{c}(s'_{1})) \ne \textit{tr}(\textit{TD}^\mathrm{c}(s'_{2}))\) – hence in any coherent resolution of \(s'\) traces \(a \, b \, c_{1}\), \(a \, b \, c_{2}\), \(a \, b \, c\) could only be executed with probability 0.5 if present, while \(s''\) admits coherent resolutions in which those traces have execution probability 0.25.

Fig. 5.
figure 5

Using weighted trace sets for coherency breaks probabilistic trace equivalence

Full size image

7 Conclusions

Based on the notion of coherent resolution of nondeterminism, presented in  [2] to avoid the anomalies of probabilistic trace semantics depicted in Fig. 3, in this paper we have provided alternative characterizations of \(\sim _\mathrm{PTr}^\mathrm{post, c}\)  [25] and \(\sim _\mathrm{PTr}^\mathrm{pre, c}\)  [3], respectively relying on the equality of fully coherent trace distributions and on the equality of coherent weighted trace sets. Both fully coherent trace distributions and coherent weighted trace sets are different from coherent trace distributions, introduced in  [2] for defining coherency constraints on resolutions.

We plan to exploit the aforementioned alternative characterizations for studying properties and decision procedures of the two examined coherency-based probabilistic trace equivalences over nondeterministic and probabilistic processes.