Compositional metric reasoning with probabilistic process calculi

Daniel Gebler, Kim Guldstrand Larsen, Simone Tini

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

18 Citations (Scopus)

Abstract

We study which standard operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We argue that uniform continuity (generalizing the earlier proposed property of non-expansiveness) captures the essential nature of compositional reasoning and allows now also to reason compositionally about recursive processes. We characterize the distance between probabilistic processes composed by standard process algebra operators. Combining these results, we demonstrate how compositional reasoning about systems specified by continuous process algebra operators allows for metric assume-guarantee like performance validation.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures : 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
EditorsAndrew Pitts
Number of pages16
PublisherSpringer
Publication date2015
Pages230-245
ISBN (Print)978-3-662-46677-3
ISBN (Electronic)978-3-662-46678-0
DOIs
Publication statusPublished - 2015
Event18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: 11 Apr 201518 Apr 2015

Conference

Conference18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Country/TerritoryUnited Kingdom
CityLondon
Period11/04/201518/04/2015
SponsorFacebook, Microsoft Research, Semmle, Springer-Verlag, Winton
SeriesLecture Notes in Computer Science
Volume9034
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Compositional metric reasoning with probabilistic process calculi'. Together they form a unique fingerprint.

Cite this