Constructive Logical Characterizations of Bisimilarity for Reactive Probabilistic Systems

Larsen and Skou characterized bisimilarity over reactive probabilistic systems with a logic including negation, conjunction, and a diamond modality decorated with a probabilistic lower bound. Later on, working on continuous state spaces, Desharnais, Edalat, and Panangaden proved that negation is not necessary to characterize the same equivalence. In this paper, we redemonstrate the former result with a simpler proof and the latter result directly on discrete state spaces without resorting to measure-theoretic arguments. Moreover, we show that conjunction can be replaced by disjunction in both logics, still characterizing the same bisimilarity. To these ends, we introduce reactive probabilistic trees, a fully abstract model for reactive probabilistic systems that allows us to uniformly prove expressiveness of the four probabilistic modal logics by means of a compactness argument. Our proofs are constructive, as they induce for each considered logic an algorithm that builds a distinguishing formula in case of two inequivalent reactive probabilistic systems.