This talk is in preparation for TACAS 2025 (paper: Efficient Evidence Generation for Modal mu-calculus Model Checking, A. Stramaglia, J. J. A. Keiren, M. Laveaux and T. A. C. Willemse).

Wesselink and Willemse[1] showed how parameterised Boolean equation systems can be extended to provide evidence explaining why the answer to a model checking problem is such.
Generating evidence can be slow. For symbolic model checking, the running time is so high that is often infeasible to generate evidence.
In this talk, I will present a two-step approach to solving PBESs that can efficiently generate evidence, using both explicit and symbolic solving techniques.

[1] Wesselink, W., Willemse, T.A.: Evidence Extraction from Parameterised Boolean Equation Systems, ARQNL 2018, pp. 86–100, Jan 2018