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

Christel BaierChristel Baier, Calvin ChauCalvin Chau, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Christel Baier, Calvin Chau, Sascha Klüppelholz
Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes
In Jane Hillston and Sadegh Soudjani and Masaki Waga, eds., Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9-13, 2024, Proceedings, volume 14996 of Lecture Notes in Computer Science, 1--18, 2024. Springer

Details
Bibtex

KurzfassungAbstract
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.
Projekt:Project: SEMECO-Q2
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-68416-6_1.

@inproceedings{BCK2024,
  author    = {Christel Baier and Calvin Chau and Sascha Kl{\"{u}}ppelholz},
  title     = {Certificates and Witnesses for Multi-objective Queries in Markov
               Decision Processes},
  editor    = {Jane Hillston and Sadegh Soudjani and Masaki Waga},
  booktitle = {Quantitative Evaluation of Systems and Formal Modeling and
               Analysis of Timed Systems - First International Joint Conference,
               {QEST+FORMATS} 2024, Calgary, {AB,} Canada, September 9-13, 2024,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {14996},
  publisher = {Springer},
  year      = {2024},
  pages     = {1--18},
  doi       = {10.1007/978-3-031-68416-6_1}
}