Maurice Laveaux: Decompositional Minimisation of Monolithic Processes


Event Details


Compositional minimisation can be an effective technique to reduce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form, each sequential process is replaced by an abstraction, simpler than the corresponding process while still preserving the property that is checked. However, this technique cannot be applied in a setting where parallel composition is first translated to a non-deterministic sequential monolithic process. The advantage of this monolithic process is that it facilitates static analysis of global behaviour. We present a technique that considers a monolithic process with data and decomposes it into two processes where each process defines behaviour for a subset of the parameters of the monolithic process. In this talk I will also highlight some of the practical considerations of this technique and the results that have been achieved so-far.