Anna Stramaglia: lpsparunfold: features and application

Event Details

Concise process models in mCRL2 can be obtained by the use of data types such as lists and structured sorts. However, the addition of structure in the process parameters negatively affects static analysis tools such as constant elimination, parameter elimination and sum elimination which consider process parameters as single units in their analysis. To address this problem, Groote and Lisser introduced a technique for flattening the structure of process parameters such that other static analysis tools can apply their transformation more effectively. This technique is implemented in the mCRL2 tool lpsparunfold. In practice, we observe that, although parameters can be unfolded, the static analysis tools do not always benefit from this unfolding. On the other hand we observe that the unfolding seems quite beneficial for symbolic reachability (lpsreach). In this talk I will introduce the lpsparunfold technique with a running example. I will talk about the relevant lpsparunfold options (with examples) and discuss the results of their application