Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints

Research output: Contribution to book/Conference proceedings/Anthology/ReportChapter in book/Anthology/ReportContributedpeer-review

Abstract

This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an MDP-variant of Farkas’ Lemma. The set of all such certificates is shown to form a polytope whose points correspond to witnessing subsystems of the model and the property. Using this correspondence we can translate the problem of finding minimal witnesses to the problem of finding vertices with a maximal number of zeros. While computing such vertices is computationally hard in general, we derive new heuristics from our formulations that exhibit competitive performance compared to state-of-the-art techniques. As an argument that asymptotically better algorithms cannot be hoped for, we show that the decision version of finding minimal witnesses is NP-complete even for acyclic Markov chains.

Details

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
EditorsArmin Biere, David Parker
PublisherSpringer, Berlin [u. a.]
Pages324–345
ISBN (print)978-3-030-45189-9
Publication statusPublished - 2020
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 12078
ISSN0302-9743

Conference

Title 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated titleTACAS 2020
Conference number
Duration25 - 30 April 2020
Degree of recognitionInternational event
Location
CityDublin
CountryIreland

External IDs

Scopus 85083956795

Keywords

Library keywords