Maurice Laveaux: Decompositional Minimization of Monolithic Processes

Event Details

Title: Decompositional Minimization of Monolithic Processes

Abstract: Compositional minimization is another established technique to tackle the state space explosion problem. This technique attempts to use the parallel processes defined in the high-level specification to obtain a reduced state space w.r.t some behavioural equivalence immediately without exploring the whole state space first. This technique would also be a useful addition for the mCRL2 toolset. However, applying this technique within the context of mCRL2 is hindered by the fact that we typically first transform the given specification into a monolithic process where all parallel composition has been removed. Avoiding this transformation is undesirable, because it facilitates various other static analysis techniques that might reduce the state space. Therefore, we propose a method to decompose the resulting monolithic process, where other simplification techniques could be applied first, into a number of parallel processes such that the compositional minimization technique is applicable again.