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

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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.

Details

OriginalspracheEnglisch
TitelQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems
Redakteure/-innenJane Hillston, Sadegh Soudjani, Masaki Waga
ErscheinungsortCham
Herausgeber (Verlag)Springer Nature Switzerland
Seiten1-18
Seitenumfang18
ISBN (elektronisch)978-3-031-68416-6
ISBN (Print)978-3-031-68415-9
PublikationsstatusVeröffentlicht - 2024
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science
Band14996
ISSN0302-9743

Konferenz

Titel1st International Joint Conference on Quantitative Evaluation of SysTems & Formal Modeling and Analysis of Timed Systems
KurztitelQEST+FORMATS 2024
Beschreibungpart of the CONFEST 2024 conference
Dauer9 - 13 September 2024
Webseite
BekanntheitsgradInternationale Veranstaltung
OrtBest Western Plus Village Park Inn
StadtCalgary
LandKanada

Externe IDs

ORCID /0000-0002-5321-9343/work/166762363
ORCID /0000-0003-1724-2586/work/166763922
ORCID /0000-0002-3437-0240/work/166765375

Schlagworte

Schlagwörter

  • Certificates, Markov cecision processes, multi-objective queries