Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914003850100736 |
|---|---|
| author | Baier, Christel Chau, Calvin Drobitko, Volodymyr Jantsch, Simon Klüppelholz, Sascha |
| author_facet | Baier, Christel Chau, Calvin Drobitko, Volodymyr Jantsch, Simon Klüppelholz, Sascha |
| contents | Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective ω-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous Büchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_17859 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes Baier, Christel Chau, Calvin Drobitko, Volodymyr Jantsch, Simon Klüppelholz, Sascha Logic in Computer Science Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective ω-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous Büchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques. |
| title | Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.17859 |