Larsen and Skou characterized probabilistic bisimilarity over reactiveudprobabilistic systems with a logic including true, negation, conjunction, and auddiamond modality decorated with a probabilistic lower bound. Later on,udDesharnais, Edalat, and Panangaden showed that negation is not necessary toudcharacterize the same equivalence. In this paper, we prove that the logicaludcharacterization holds also when conjunction is replaced by disjunction, withudnegation still being not necessary. To this end, we introduce reactiveudprobabilistic trees, a fully abstract model for reactive probabilistic systemsudthat allows us to demonstrate expressiveness of the disjunctive probabilisticudmodal logic, as well as of the previously mentioned logics, by means of audcompactness argument.
展开▼
