Compositional metric reasoning with probabilistic process calculi

DOI10.1007/978-3-662-46678-0_15MaRDI QIDQ2949442zbMATH OpenOpenAlexFDO

Authors Daniel Gebler, Simone Tini, Kim G. Larsen

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.06162

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

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.

Recommendations

• Compositional bisimulation metric reasoning with Probabilistic Process Calculi
• Fixed-point characterization of compositionality properties of probabilistic processes combinators
• Approximate reasoning for real-time probabilistic processes
• Sós specifications of probabilistic systems by uniformly continuous operators
• SOS specifications for uniformly continuous operators

Cited in

(16)

• SOS specifications for uniformly continuous operators
• A probabilistic calculus of cyber-physical systems
• Logical characterization of branching metrics for nondeterministic probabilistic transition systems
• Compositional bisimulation metric reasoning with Probabilistic Process Calculi
• Metric reasoning about -terms: the general case
• Equational reasonings in wireless network gossip protocols
• SOS-based modal decomposition on nondeterministic probabilistic processes
• Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice
• Fixed-point characterization of compositionality properties of probabilistic processes combinators
• Compositional weak metrics for group key update
• Approximate reasoning for real-time probabilistic processes
• Sós specifications of probabilistic systems by uniformly continuous operators
• Up-to techniques for behavioural metrics via fibrations
• Fully Syntactic Uniform Continuity Formats for Bisimulation Metrics
• Contextual behavioural metrics
• Logical characterization of bisimulation metrics

This page was built for publication: Compositional metric reasoning with probabilistic process calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2949442)