Jeroen Keiren: Towards effective unfolding of structured parameters in mCRL2

Event Details

Data types such as lists and structured sorts enable the creation of concise process models in mCRL2. However, static analysis tools such as constant elimination, parameter elimination and sum elimination only consider process parameters as a single unit in their analysis. Therefore, the added structure in process parameters negatively affects these static analysis techniques. Groote and Lisser introduced a technique for flattening the structure of process parameters, implemented in the mCRL2 tool lpsparunfold. This tools replaces a single structured process parameter by multiple parameters. In practice, we often observe that, although parameters can be unfolded, the static analysis tools do not benefit from this unfolding. In this talk I will explain parameter unfolding and show some examples of how it falls short in practice. I will also discuss ideas for improvements, and the correctness criteria that parameter unfolding should satisfy.