Modal Logic Characterization of Markovian Testing and Trace Equivalences

Markovian testing and trace equivalences have been recently proposed as reasonable alternatives to Markovian bisimilarity, as both of them induce at the Markov chain level an aggregation strictly coarser than ordinary lumping that is still exact. In this paper we provide a modal logic characterization for each of the two non-bisimulation-based Markovian behavioral equivalences, which relies on a quantitative interpretation of a variant of the Hennessy-Milner logic. We also show that, unlike the Markovian bisimilarity case, such modal logic characterizations exist only when probabilistic and temporal aspects are treated in a global way.