Probabilistic Bisimulation for Realistic Schedulers

Autor: Eisentraut, Christian, Godskesen, Jens Christian, Hermanns, Holger, Song, Lei, Zhang, Lijun
Jazyk: angličtina
Rok vydání: 2015
Předmět:
Zdroj: Eisentraut, C, Godskesen, J C, 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
DOI: 10.1007/978-3-319-19249-9_16
Popis: 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.
Databáze: OpenAIRE