Constructive logical characterizations of bisimilarity for reactive probabilistic systems (Q1731513)

Larsen and Skou characterized bisimilarity over reactive probabilistic systems (every state has for each action at most one outgoing distribution over states) with a logic including negation, conjunction, and a diamond modality \(\langle a \rangle_p \phi\) (which is satisfied by a state if, after performing action \(a\), the probability of being in a state satisfying \(\phi\) is at least \(p\)). Later on, working on continuous state spaces, Desharnais, Edalat, and Panangaden proved that negation is not necessary to characterize the same equivalence. The former result is demonstrated with a simpler proof and the latter result directly on discrete state spaces without resorting to measure-theoretic arguments. Moreover, it is shown that conjunction can be replaced by disjunction in both logics, still characterizing the same bisimilarity. 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, are introduced. The presented proofs are constructive as they induce for each considered logic an algorithm that builds a distinguishing formula in the case of two inequivalent reactive probabilistic systems.