2013/10/02 by Matteo Mio, Mio, Matteo
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1310.0768
openalex publication_date 2013/10/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.