Upper-Expectation Bisimilarity and Real-valued Modal Logics

TL;DR

This paper introduces upper-expectation bisimilarity, a new behavioral equivalence for probabilistic systems, with logical characterizations and proof of congruence, unifying and extending existing notions.

Contribution

It develops the theory of upper-expectation bisimilarity, showing its equivalence to convex bisimilarity for many systems and providing logical characterizations.

Findings

Upper-expectation bisimilarity coincides with convex bisimilarity in many cases.

Logical characterizations include probabilistic modal mu-calculi and a real-valued modal logic.

Proven to be a congruence for probabilistic process algebras.

Abstract

Several notions of bisimulation relations for probabilistic non-deterministic transition systems have been considered in the literature. We consider a novel testing-based behavioral equivalence called upper-expectation bisimilarity and develop its theory using standard results from linear algebra and functional analysis. We show that, for a wide class of systems, our new notion coincides with Segala's convex bisimilarity. We develop logical characterizations in terms of expressive probabilistic modal mu-calculi and a novel real-valued modal logic. We prove that upper-expectation bisimilarity is a congruence for the wide family of process algebras specified following the probabilistic GSOS rule format.