Compositional bisimulation metric reasoning with Probabilistic Process Calculi

DOI10.2168/LMCS-12(4:12)2016zbMath1398.68365MaRDI QIDQ2974795

Simone Tini, Daniel Gebler, Kim Guldstrand Larsen

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

uniform continuitycompositional reasoningprobabilistic process algebrabisimulation metric semantics

Mathematics Subject Classification ID

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)

Related Items

A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces, Differential logical relations. II: Increments and derivatives, SOS specifications for uniformly continuous operators, A framework to measure the robustness of programs in the unpredictable environment, Back to the format: a survey on SOS for probabilistic processes, Up-to techniques for behavioural metrics via fibrations, Up-To Techniques for Behavioural Metrics via Fibrations, The metric linear-time branching-time spectrum on nondeterministic probabilistic processes, Probabilistic divide \& congruence: branching bisimilarity, Unnamed Item, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Unnamed Item, A probabilistic calculus of cyber-physical systems, Monads and Quantitative Equational Theories for Nondeterminism and Probability, Compositional weak metrics for group key update, How adaptive and reliable is your program?

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity
• On behavioural pseudometrics and closure ordinals
• Metrics for labelled Markov processes
• SOS formats and meta-theory: 20 years after
• Non-expansive \(\varepsilon\)-bisimulations for probabilistic processes
• Bisimulation through probabilistic testing
• Turning SOS rules into equations
• A logic for reasoning about time and reliability
• A behavioural pseudometric for probabilistic transition systems
• Compositionality of Hennessy-Milner logic by structural operational semantics
• The quantitative linear-time-branching-time spectrum
• Computing Behavioral Distances, Compositionally
• Remarks on Testing Probabilistic Processes
• Probabilistic Barbed Congruence
• Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation
• Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
• Probabilistic bisimulation as a congruence
• Compositional Metric Reasoning with Probabilistic Process Calculi
• Generalized Bisimulation Metrics
• Formal verification of parallel programs
• Bisimulation can't be traced
• Modal Decomposition on Nondeterministic Probabilistic Processes
• A Proof System for Compositional Verification of Probabilistic Concurrent Processes
• SOS specifications of probabilistic systems by uniformly continuous operators
• Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus
• Non Expansive ε-Bisimulations