Behavioural pseudometrics for nondeterministic probabilistic systems

Wenjie Du, Yuxin Deng, Daniel Gebler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

17 Scopus citations

Abstract

For the model of probabilistic labelled transition systems that allow for the co-existence of nondeterminism and probabilities, we present two notions of bisimulation metrics: one is state-based and the other is distribution-based. We provide a sound and complete modal characterisation for each of them, using real-valued modal logics based on Hennessy-Milner logic. The logic for characterising the state-based metric is much simpler than an earlier logic by Desharnais et al. as it uses only two non-expansive operators rather than the general class of nonexpansive operators. For the kernels of the two metrics, which correspond to two notions of bisimilarity, we give a comprehensive comparison with some typical distribution-based bisimilarities in the literature.

Original languageEnglish
Title of host publicationDependable Software Engineering
Subtitle of host publicationTheories, Tools, and Applications - 2nd International Symposium, SETTA 2016, Proceedings
EditorsMartin Franzle, Deepak Kapur, Naijun Zhan
PublisherSpringer Verlag
Pages67-84
Number of pages18
ISBN (Print)9783319476766
DOIs
StatePublished - 2016
Event2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, China
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9984 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
Country/TerritoryChina
CityBeijing
Period9/11/1611/11/16

Fingerprint

Dive into the research topics of 'Behavioural pseudometrics for nondeterministic probabilistic systems'. Together they form a unique fingerprint.

Cite this