Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Christel Baier, Calvin Chau, Sascha Klüppelholz

TL;DR

This paper addresses certifying certificates and witnesses for multi-objective queries in Markov decision processes, focusing on reachability-invariant and mean-payoff objectives. It develops a certifying framework based on Farkas' lemma, constructs a product MDP and its MEC quotient to reduce to a reachability form, and establishes a direct link between certificates, witnessing schedulers, and minimal subsystems. The authors also provide a transfer mechanism to lift witnesses from the MEC quotient back to the original MDP, and they implement and experimentally evaluate the approach, including MILP-based minimization of witnessing subsystems. The work enhances trust and explainability in multi-objective verification by yielding concise certificates and actionable witnesses, with practical utility demonstrated through prototype tooling and benchmarks.

Abstract

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.

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

TL;DR

This paper addresses certifying certificates and witnesses for multi-objective queries in Markov decision processes, focusing on reachability-invariant and mean-payoff objectives. It develops a certifying framework based on Farkas' lemma, constructs a product MDP and its MEC quotient to reduce to a reachability form, and establishes a direct link between certificates, witnessing schedulers, and minimal subsystems. The authors also provide a transfer mechanism to lift witnesses from the MEC quotient back to the original MDP, and they implement and experimentally evaluate the approach, including MILP-based minimization of witnessing subsystems. The work enhances trust and explainability in multi-objective verification by yielding concise certificates and actionable witnesses, with practical utility demonstrated through prototype tooling and benchmarks.

Abstract

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.
Paper Structure (5 sections, 6 theorems, 3 figures)

This paper contains 5 sections, 6 theorems, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Certificates and Witnesses for ReachInv-Queries
  4. Farkas Certificates and Witnesses for Reach-Queries
  5. Transferring Witnesses

Key Result

lemma thmcounterlemma

Let $\mathbf{A} \in \mathbb{R}^{m \times n}$ and $\mathbf{b} \in \mathbb{R}^{m}$, then the following holds:

Figures (3)

  • Figure 1: Overview of our approach for ReachInv-queries.
  • Figure 2: MILPs for finding minimal witnessing subsystems for Reach-queries.
  • Figure 3: Grayed-out states are not in the subsystem and transitions leading there are redirected to a fresh $\bot$ state. For readability, some action names are omitted.

Theorems & Definitions (9)

  • lemma thmcounterlemma: Farkas' lemma (e.g. Proposition 6.4.3 in matousek_understanding_2007)
  • lemma thmcounterlemma: Certificates for -queries
  • proof : Sketch
  • lemma thmcounterlemma: Farkas certificates for -queries
  • proof : Sketch
  • remark thmcounterremark
  • theorem thmcountertheorem: Monotonicity
  • theorem thmcountertheorem
  • lemma thmcounterlemma