Visualising CSP Compressions
Supervisors
Suitable for
Abstract
FDR3 has a number of inbuilt compression functions, such as normal, diamond and sbisim, that aim to reduce the number of states in the system. Typically, compressions can yield substantial reductions in the number of states, and thus the time taken to check a particular problem, but it can be somewhat difficult to reason about why a compression does or does not work. The aim of this project would be to produce a tool that allows the results of a compression function to be visualised, in order to allow a user to understand why a compression is or is not working. Essentially, the tool would display both the original CSP process (as a labelled transition system), and the resulting compressed transition system, and would provide a way of indicating how the states of the two systems are related. This tool would build on top of the compression functions of FDR3 [1], and would hopefully be integrated on successful completion. This project would require the Concurrency course. Some knowledge of computer graphics concepts would be useful, but not required.
[1] FDR3: https://www.cs.ox.ac.uk/projects/fdr/