Constructive logical characterizations of bisimilarity for reactive probabilistic systems
type: Item
instance of: scholarly article
title: Constructive logical characterizations of bisimilarity for reactive probabilistic systems
zbMATH Open document ID: 1476.68165
author: Marco Bernardo
author: Marino Miculan
published in: Theoretical Computer Science
publication date: 2019-03-13T00:00:00Z
review text: 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.
reviewed by: Damas Gruska
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 68Q87
zbMATH DE Number: 7035846
zbMATH Keywords: bisimilarity
zbMATH Keywords: reactive probabilistic systems
zbMATH Keywords: modal logic characterizations
MaRDI profile type: Publication
full work available at URL: j.tcs.2018.12.003
OpenAlex ID: W2904057364
cites work: A final coalgebra theorem
cites work: Domain equations for probabilistic processes
cites work: Q4836494
cites work: Q4037401
cites work: Equivalence and preorder checking for finite-state systems
cites work: Bisimulation and cocongruence for probabilistic systems
cites work: Finite state Markovian decision processes
cites work: Bisimulation for labelled Markov processes
cites work: Approximating labelled Markov processes
cites work: Q5111437
cites work: The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
cites work: Reactive, generative, and stratified models of probabilistic processes
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Exemplaric Expressivity of Modal Logics
cites work: CCS expressions, finite state processes, and three problems of equivalence
cites work: Formal verification of parallel programs
cites work: Q3262596
cites work: Bisimulation through probabilistic testing
cites work: Q3992568
cites work: Probabilistic automata
cites work: Universal coalgebra: A theory of systems
cites work: Bisimulation for probabilistic transition systems: A coalgebraic approach
cites work: On the final sequence of a finitary set functor
Wikidata QID: Q128821272
DOI: 10.1016/J.TCS.2018.12.003
description: scientific article; zbMATH DE number 7035846