Uniform Logical Characterizations of Testing Equivalences for Nondeterministic, Probabilistic and Markovian Processes

Logical characterizations of nondeterministic, probabilistic, and Markovian variants of bisimulation equivalence rely on similar modal languages, each including true, negation, conjunction, and diamond. Likewise, logical characterizations of the corresponding variants of trace equivalence rely on similar modal languages, each including only true and diamond. Unfortunately, this is not the case with the existing logical characterizations of the corresponding variants of testing equivalence, as they are based on different modal languages. In this paper we show that the logical characterizations of testing equivalences for fully nondeterministic processes, fully probabilistic processes, and fully Markovian processes without silent moves can be harmonized by means of a modal language comprising true, disjunction, and diamond.