Probabilistic Bisimulation for Realistic Schedulers

Christian  Eisentraut; Jens Christian Godskesen; Holger  Hermanns; Lei Song; Lijun Zhang

doi:10.1007/978-3-319-19249-9_16

Probabilistic Bisimulation for Realistic Schedulers

Christian Eisentraut, Jens Christian Godskesen, Holger Hermanns, Lei Song, Lijun Zhang

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

Abstract

Weak distribution bisimilarity is an equivalence notion on probabilistic automata, originally proposed for Markov automata. It has gained some popularity as the coarsest behavioral equivalence enjoying valuable properties like preservation of trace distribution equivalence and compositionality. This holds in the classical context of arbitrary schedulers, but it has been argued that this class of schedulers is unrealistically powerful. This paper studies a strictly coarser notion of bisimilarity, which still enjoys these properties in the context of realistic subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of behavioral semantics.

Originalsprog	Engelsk
Titel	FM 2015: Formal Methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
Vol/bind	9109
Forlag	Springer
Publikationsdato	2015
Sider	248-264
ISBN (Trykt)	978-3-319-19248-2
ISBN (Elektronisk)	978-3-319-19249-9
DOI	https://doi.org/10.1007/978-3-319-19249-9_16
Status	Udgivet - 2015
Begivenhed	The 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norge Varighed: 22 jun. 2015 → 26 jun. 2015 Konferencens nummer: 20 http://fm2015.ifi.uio.no/

Konference

Konference	The 20th International Symposium on Formal Methods
Nummer	20
Lokation	University of Oslo
Land/Område	Norge
By	Oslo
Periode	22/06/2015 → 26/06/2015
Internetadresse	http://fm2015.ifi.uio.no/

Navn	Lecture Notes in Computer Science
ISSN	0302-9743

Emneord

Probabilistic automata
Weak distribution bisimilarity
Behavioral equivalence
Partial information schedulers
Compositional theory

Adgang til dokumentet

10.1007/978-3-319-19249-9_16

MEALS-Deliverable-1.3-2Accepteret manuskript, 209 KB

http://link.springer.com/chapter/10.1007%2F978-3-319-19249-9_16

Citationsformater

@inproceedings{3207380d143d42dc83a859f655c4d42c,

title = "Probabilistic Bisimulation for Realistic Schedulers",

abstract = "Weak distribution bisimilarity is an equivalence notion on probabilistic automata, originally proposed for Markov automata. It has gained some popularity as the coarsest behavioral equivalence enjoying valuable properties like preservation of trace distribution equivalence and compositionality. This holds in the classical context of arbitrary schedulers, but it has been argued that this class of schedulers is unrealistically powerful. This paper studies a strictly coarser notion of bisimilarity, which still enjoys these properties in the context of realistic subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of behavioral semantics.",

keywords = "Probabilistic automata, Weak distribution bisimilarity, Behavioral equivalence, Partial information schedulers, Compositional theory, Probabilistic automata, Weak distribution bisimilarity, Behavioral equivalence, Partial information schedulers, Compositional theory",

author = "Christian Eisentraut and Godskesen, {Jens Christian} and Holger Hermanns and Lei Song and Lijun Zhang",

year = "2015",

doi = "10.1007/978-3-319-19249-9_16",

language = "English",

isbn = "978-3-319-19248-2",

volume = "9109",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "248--264",

booktitle = "FM 2015: Formal Methods",

address = "Germany",

note = "The 20th International Symposium on Formal Methods, FM 2015 ; Conference date: 22-06-2015 Through 26-06-2015",

url = "http://fm2015.ifi.uio.no/",

}

Eisentraut, C, Godskesen, JC, Hermanns, H, Song, L & Zhang, L 2015, Probabilistic Bisimulation for Realistic Schedulers. i FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. bind 9109, Springer, Lecture Notes in Computer Science, s. 248-264, The 20th International Symposium on Formal Methods, Oslo, Norge, 22/06/2015. https://doi.org/10.1007/978-3-319-19249-9_16

Probabilistic Bisimulation for Realistic Schedulers. / Eisentraut, Christian; Godskesen, Jens Christian; Hermanns, Holger et al.
FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Bind 9109 Springer, 2015. s. 248-264 (Lecture Notes in Computer Science).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Probabilistic Bisimulation for Realistic Schedulers

AU - Eisentraut, Christian

AU - Godskesen, Jens Christian

AU - Hermanns, Holger

AU - Song, Lei

AU - Zhang, Lijun

N1 - Conference code: 20

PY - 2015

Y1 - 2015

N2 - Weak distribution bisimilarity is an equivalence notion on probabilistic automata, originally proposed for Markov automata. It has gained some popularity as the coarsest behavioral equivalence enjoying valuable properties like preservation of trace distribution equivalence and compositionality. This holds in the classical context of arbitrary schedulers, but it has been argued that this class of schedulers is unrealistically powerful. This paper studies a strictly coarser notion of bisimilarity, which still enjoys these properties in the context of realistic subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of behavioral semantics.

AB - Weak distribution bisimilarity is an equivalence notion on probabilistic automata, originally proposed for Markov automata. It has gained some popularity as the coarsest behavioral equivalence enjoying valuable properties like preservation of trace distribution equivalence and compositionality. This holds in the classical context of arbitrary schedulers, but it has been argued that this class of schedulers is unrealistically powerful. This paper studies a strictly coarser notion of bisimilarity, which still enjoys these properties in the context of realistic subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of behavioral semantics.

KW - Probabilistic automata

KW - Weak distribution bisimilarity

KW - Behavioral equivalence

KW - Partial information schedulers

KW - Compositional theory

KW - Probabilistic automata

KW - Weak distribution bisimilarity

KW - Behavioral equivalence

KW - Partial information schedulers

KW - Compositional theory

U2 - 10.1007/978-3-319-19249-9_16

DO - 10.1007/978-3-319-19249-9_16

M3 - Article in proceedings

SN - 978-3-319-19248-2

VL - 9109

T3 - Lecture Notes in Computer Science

SP - 248

EP - 264

BT - FM 2015: Formal Methods

PB - Springer

T2 - The 20th International Symposium on Formal Methods

Y2 - 22 June 2015 through 26 June 2015

ER -

Probabilistic Bisimulation for Realistic Schedulers

Abstract

Konference

Emneord

Adgang til dokumentet

Fingeraftryk

Citationsformater