Willemse and Wesselink extended the PBES solvers in the mCRL2 toolset to support extracting evidence (witnesses and counterexamples) in the form a subsystems of a labelled transition system. This extension requires adding additional information to the PBES. Stramaglia has previously shown 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.

In this talk, I will explain how we use this two-step approach in the symbolic PBES solving pbessolvesymbolic.