Abstract Model checking is a technique to automatically establish whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its requirements is essential for the user to understand the model checking result. Willemse and Wesselink showed that parameterised Boolean equation systems (PBESs), an intermediate format for $$\mu $$ μ -calculus model checking, can be extended with information to generate such evidence. Solving the resulting PBES is much slower than solving one without additional information, and sometimes even impossible. In this paper we develop a two-step approach to solving a PBES with additional information: we first solve its core and subsequently use the information obtained in this step to solve the PBES with additional information. We prove the correctness of our approach and we have implemented it, demonstrating that it efficiently generates evidence using both explicit and symbolic solving techniques.

When describing the behavior of systems, state variables are typically modeled using complex data types. This use of data types allows for concise models that are easy to read. However, model checking tools that aim to automatically establish the correctness of such models use static analyses of state variables to improve their performance. Therefore, the use of complex data types in behavioral models negatively affects the performance of model checking tools. To address this, in this article we revisit a technique by Groote and Lisser that can be used to replace a single state variable of a complex data type by multiple state variables of simpler data types. We introduce and study several extensions in the context of the process algebraic specification language mCRL2, and establish their correctness. We demonstrate that our technique typically reduces the verification times when using symbolic model checking, and show that sometimes it enables static analysis to reduce the underlying state space from infinite to finite.