Complex abstract data types are often used to facilitate creating concise models of the behavior of realistic systems. However, static analysis techniques that aim to optimize such models often consider variables of complex types as a single indivisible unit. The use of complex data types thus negatively affects the optimizations that can be performed.
To address this problem, Groote and Lisser introduced a technique for flattening the structure of process parameters, then implemented in mCRL2 in the tool lpsparunfold. We have extended the technique behind lpsparufold and implemented the changes.
In this talk I will first introduce the original lpsparunfold technique by Groote and Lisser (with an example), then describe our extensions (with examples) and finally discuss the results of the application of our extended technique on various specifications from different domains.
This is joint work with Jeroen Keiren and Thomas Neele.