  Certifying verification algorithms not only return whether a given property
holds or not, but also provide an accompanying independently checkable
certificate and a corresponding witness. The certificate can be used to easily
validate the correctness of the result and the witness provides useful
diagnostic information, e.g. for debugging purposes. Thus, certificates and
witnesses substantially increase the trustworthiness and understandability of
the verification process. In this work, we consider certificates and witnesses
for multi-objective reachability-invariant and mean-payoff queries in Markov
decision processes, that is conjunctions or disjunctions either of reachability
and invariant or mean-payoff predicates, both universally and existentially
quantified. Thereby, we generalize previous works on certificates and witnesses
for single reachability and invariant constraints. To this end, we turn known
linear programming techniques into certifying algorithms and show that
witnesses in the form of schedulers and subsystems can be obtained. As a
proof-of-concept, we report on implementations of certifying verification
algorithms and experimental results.
