Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes

Christel Baier, Calvin Chau, Sascha Klüppelholz

Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding w…