Title: Probabilistic Resources
Speakers: Filip Smola
Abstract:

When composing processes, non-deterministic resources allow us to express uncertainty such as decisions, sensing or possible failure. However, in practice we want to know not only the possible cases but also their relative probabilities. We may use these to compute the expected value of some performance metric or to uncover impossible execution paths.

In this talk I will present our work on adding these probabilities to a theory of process composition mechanised in Isabelle/HOL. I will give a high-level overview of how the probabilistic information is represented, the issues we encounter and how we address those.