Supervisors

Suitable for

Abstract

Prerequisites: 

Concurrency, Verification

 

Background

PRISM [1] is a probabilistic model checking tool that enables the formal modelling and verification of systems that exhibit probabilistic behaviours. It is widely regarded as an influential tool (2016 HVC Award at the Haifa Verification Conference) in the domain of verification, particularly for stochastic systems, due to its powerful modelling capabilities and efficient algorithms for analysing probabilistic properties. The PRISM language allows users to specify states, transitions, and probabilistic choices, as well as properties that are to be verified, such as safety, liveness, and performance. Properties are expressed in probabilistic temporal logics such as PCTL (Probabilistic Computation Tree Logic) and LTL (Linear Temporal Logic).

There is much work on probabilistic bisimularity 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

PRISM-games [2] allows for the verification of probabilistic systems that can incorporate competitive or collaborative behaviour, modelled as stochastic multi-player games. There is a well-studied relation between bisimulation and game semantics. Our goal is to use PRISM-games to model check probabilistic bisimulation. Further work in benchmarking efficiency and expressing multiple probabilistic definitions of bisimulations and evaluating them both on expressivity and implementation.

Method

There is a wealth of research on this topic. For example, [3] gives a definition for weak probabilistic bisimulation of labelled concurrent markov chains along with a method on deciding if two systems are bisimilar. Similarly [4] gives similar results in the field of probabilistic automata. We will focus on the former, first modelling Labelled Concurrent Markov Chain (LCMC) can model checking them in PRISM-games.

 

[1] PRISM - Probabilistic Symbolic Model Checker

[2] PRISM-games

[3] Weak Bisimulation for Probabilistic Systems | SpringerLink

[4] Language Equivalence for Probabilistic Automata | SpringerLink