Bisimulation Algorithmics (available)

Starting Date: June /July 2023
Prerequisites: Interest in functional programming (OCaml specially)
Will results be assigned to University: No

Labelled transition systems are a crucial abstraction to understand
complex and distributed systems. Bisimulation, in its many variations,
is conceptually at the core of many verification tools. One such tool
is OvenMPST. OvenMPST is a tool for validating
and handling multiparty protocol specifications. In this tool,
bisimulation plays a central role in establishing that a protocol is
well formed and correctly specified. The objective of this project, is
to take the existing naive implementation of bisimulation to the next
level. Fortunately, there are several well known techniques that can
be adapted to this setting, and be subsequently implemented.

The tool is implemented in the OCaml functional programming language,
that is compiled to JavaScript and deployed to the web (there is also
a command line interface available). This project will consist on
understanding how to efficiently implement bisimulation, and then
implement improvements in OvenMPST, and finally, validate that the
performance improved (and correctness preserved, or even improved).
All in all, it is a challenging opportunity to learn functional
programming, how to implement an important (but well known) algorithm,
and how to measure improvements in a small preexisting code base.