Constructive logical characterizations of bisimilarity for reactive probabilistic systems