PSTMonitor: Monitor Synthesis from Probabilistic Session Types
Christian Bartolo Burl\`o, Adrian Francalanza, Alceste Scalas, Catia, Trubiani, Emilio Tuosto

TL;DR
PSTMonitor is a tool that verifies message-passing applications at runtime by checking if their probabilistic behaviour aligns with specified session types, analyzing its feasibility and overhead.
Contribution
It introduces PSTMonitor, a novel runtime verification tool for probabilistic session types in message-passing systems, including an analysis of its overhead.
Findings
PSTMonitor effectively detects deviations from expected probabilistic behaviour.
The tool's runtime overhead is manageable for practical applications.
PSTMonitor demonstrates feasibility in real-world scenarios.
Abstract
We present PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types. The key element of PSTMonitor is the detection of executions that deviate from expected probabilistic behaviour. Besides presenting PSTMonitor and its operation, the paper analyses its feasibility in terms of the runtime overheads it induces.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
