Certificates and witnesses for multi-objective queries in Markov decision processes

Research output: Contribution to journalResearch articleContributedpeer-review

Abstract

Probabilistic model checking is a technique for formally verifying the correctness of probabilistic systems w.r.t. given specifications. Typically, a model checking procedure outputs whether a specification is satisfied or not, but does not provide additional insights on the correctness of the result, thereby diminishing the trustworthiness and understandability of the verification process. In this work, we consider certifying verification algorithms that also provide an independently checkable certificate and witness in addition to the verification result. 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. More specifically, we study certificates and witnesses for specifications in the form of multi-objective queries in Markov decision processes. We first consider multi-objective reachability and invariant queries and then extend our techniques to mean-payoff expectation and mean-payoff percentile queries. Thereby, we generalize previous works on certificates and witnesses for single reachability and invariant constraints. In essence, we derive certifying verification algorithms from known linear programming techniques and show that witnesses, both in the form of schedulers and subsystems, can be obtained from the certificates. As a proof-of-concept, we report on an implementation of our certifying verification algorithms and present experimental results, demonstrating the applicability on moderately-sized case studies.

Details

Original languageEnglish
Article number102482
JournalPerformance Evaluation
Volume168
Publication statusPublished - Jun 2025
Peer-reviewedYes

External IDs

Scopus 105001391522
ORCID /0000-0002-5321-9343/work/182726222
ORCID /0000-0003-1724-2586/work/182728840

Keywords

Keywords

  • Multi-objective queries, Markov decision processes, Certificates