Model checking is a technique to automatically assess the quality of software and hardware systems.
Given a system specification and a requirement, a model checker returns the answer to the model checking problem, true or false.
In case the result is not as expected the model checker desireably provides evidence to explain why the answer is such.
In the context of mCRL2, we use Parameterised Boolean Equation Systems (PBESs) to encode the model checking problem for the first-order modal μ-calculus.
For explicit model checking we are also able to provide evidence [1].
We are not yet able to do so for symbolic model checking.
In this talk, by means of a running example, I will describe a new approach to optimize evidence extraction from PBESs in the explicit setting.
I will also describe our ideas on how to integrate this to the symbolic setting.
This presentation is based on joint work (in progress) with Jeroen Keiren and Tim Willemse.
[1] Wesselink, W., Willemse, T.A.: Evidence extraction from parameterised Boolean
equation systems, ARQNL 2018, pp. 86–100, Jan 2018