  In this paper we continue our research line on logical characterizations of
behavioral metrics obtained from the definition of a metric over the set of
logical properties of interest. This time we provide a characterization of both
strong and weak trace metric on nondeterministic probabilistic processes, based
on a minimal boolean logic L which we prove to be powerful enough to
characterize strong and weak probabilistic trace equivalence. Moreover, we also
prove that our characterization approach can be restated in terms of a more
classic probabilistic L-model checking problem.
