Constructive logical characterizations of bisimilarity for reactive probabilistic systems (Q1731513): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2018.12.003 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2904057364 / rank | |||
Normal rank |
Revision as of 02:48, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Constructive logical characterizations of bisimilarity for reactive probabilistic systems |
scientific article |
Statements
Constructive logical characterizations of bisimilarity for reactive probabilistic systems (English)
0 references
13 March 2019
0 references
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.
0 references
bisimilarity
0 references
reactive probabilistic systems
0 references
modal logic characterizations
0 references