Semantisches Browsen
Aus International Center for Computational Logic
Certifying verification algorithms not onl … 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.ation algorithms and experimental results. +
@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}
}
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}
}
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 +
Baier +
Christel +
Christel Baier, Calvin Chau, Sascha Klüppe … Christel Baier, Calvin Chau, Sascha Klüppelholz<br/> '''[[Inproceedings3474879216|<b>Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes</b>]]''' <br/>__NOTOC__In Jane Hillston and Sadegh Soudjani and Masaki Waga, eds., <i>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</i>, volume 14996 of Lecture Notes in Computer Science, 1--18, 2024. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings3474879216|Details]]ngs3474879216|Details]] +
Christel Baier, Calvin Chau, Sascha Klüppe … Christel Baier, Calvin Chau, Sascha Klüppelholz<br/> '''[[Inproceedings3474879216/en|<b>Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes</b>]]''' <br/>__NOTOC__In Jane Hillston and Sadegh Soudjani and Masaki Waga, eds., <i>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</i>, volume 14996 of Lecture Notes in Computer Science, 1--18, 2024. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings3474879216|Details]]ngs3474879216|Details]] +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
18. März 2025, 13:07:58 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +, Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +, Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +, Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +, Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +, Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes + und Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes +
