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

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › 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.

Original language	English
Title of host publication	FM 2015: Formal Methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
Volume	9109
Publisher	Springer
Publication date	2015
Pages	248-264
ISBN (Print)	978-3-319-19248-2
ISBN (Electronic)	978-3-319-19249-9
DOIs	https://doi.org/10.1007/978-3-319-19249-9_16
Publication status	Published - 2015
Event	The 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norway Duration: 22 Jun 2015 → 26 Jun 2015 Conference number: 20 http://fm2015.ifi.uio.no/

Conference

Conference	The 20th International Symposium on Formal Methods
Number	20
Location	University of Oslo
Country/Territory	Norway
City	Oslo
Period	22/06/2015 → 26/06/2015
Internet address	http://fm2015.ifi.uio.no/

Series	Lecture Notes in Computer Science
ISSN	0302-9743

Access to Document

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

MEALS-Deliverable-1.3-2Accepted author manuscript, 209 KB

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

Cite this

@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.",

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. in FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. vol. 9109, Springer, Lecture Notes in Computer Science, pp. 248-264, The 20th International Symposium on Formal Methods, Oslo, Norway, 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. Vol. 9109 Springer, 2015. p. 248-264 (Lecture Notes in Computer Science).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › 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.

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

Conference

Access to Document

Fingerprint

Cite this