Supervisors

Suitable for

Abstract

Prerequisites:  Concurrency

 

Background

In probabilistic concurrent process algebras typically probabilistic choice is expressed in one of two ways, the first being attaching a probability value to an explicit nondeterministic choice operator, this can be seen as the process flipping a coin with some bias and behaving dependant on the outputted result such as in [1] (defined on binary session types) where a flip operator is given. Here the focus is on reasoning about expected resource consumption on a system being inferred at type checking. Another implementation can be seen in [2] where an explicit nondeterministic choice is annotated with a probability. Similarly, session types are annotated with probabilities (internal and external choice) allowing for extended reasoning on termination derived from typing.

The second formulation has been to attach probabilities to selection behaviours such as in [3] which reasons about probabilistic session types from the top-down perspective. The system allows for both probabilistic choices made internally by a process as well as nondeterministic choices which is made externally.

There is much work on probabilistic bisimilarity that has been applied to both Markov decision processes and probabilistic automata. Probabilistic bisimulation is an extension of traditional bisimulation. While the concept itself is theoretically elegant, computing and reasoning about probabilistic bisimulation is significantly more challenging than its non-probabilistic counterpart due to the need to compare probability distributions over transitions, rather than simply matching states. Hence algorithms involved are computationally intensive, making probabilistic bisimulation harder to compute and verify.

Focus

We want to reason about behaviour equivalences between probabilistic multiparty protocols. The goal of this project it to define what it means for global protocols to be probabilistically bisimular to each other and relate it with existing work.

Method

There is a wealth of research on this topic. For example, [4] gives a definition for weak probabilistic bisimulation of labelled concurrent Markov chains along with a method on deciding if two systems are bisimular. Similarly [5] gives similar results in the field of probabilistic automata. Simularly [3] gives a method of expressing global protocols. Combining these two techniques we aim to give a satisfactory definition and evaluate its relative expressiveness.

 

[1] Probabilistic Resource-Aware Session Types

[2] Probabilistic Analysis of Binary Sessions

[3] 1909.01748v1

[4] Weak Bisimulation for Probabilistic Systems | SpringerLink

[5] Language Equivalence for Probabilistic Automata | SpringerLink