Towards Probabilistic Session-Type Monitoring

TL;DR

This paper introduces a tool for runtime analysis of communicating processes using probabilistic session types, which monitors process behavior, infers probabilistic patterns, and detects deviations from expected behavior.

Contribution

It proposes a novel approach to probabilistic session type monitoring by synthesizing a runtime monitor from probabilistic session specifications.

Findings

Effective detection of behavioral deviations

Successful synthesis of probabilistic monitors

Enhanced runtime analysis capabilities

Abstract

We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is decorated by a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviates from the one specified by the probabilistic session type.