Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints

Florian FunkeFlorian Funke, Simon JantschSimon Jantsch, Christel BaierChristel Baier

DOI Link

Florian Funke, Simon Jantsch, Christel Baier
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
In Armin Biere and David Parker, eds., Proc. of 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 12078 of Lecture Notes in Computer Science, 324--345, 2020. Springer

Details
Bibtex

KurzfassungAbstract
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 -complete even for acyclic Markov chains.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-45190-5_18.

@inproceedings{FJB2020,
  author    = {Florian Funke and Simon Jantsch and Christel Baier},
  title     = {Farkas Certificates and Minimal Witnesses for Probabilistic
               Reachability Constraints},
  editor    = {Armin Biere and David Parker},
  booktitle = {Proc. of 26th International Conference on Tools and Algorithms
               for the Construction and Analysis of Systems (TACAS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12078},
  publisher = {Springer},
  year      = {2020},
  pages     = {324--345},
  doi       = {10.1007/978-3-030-45190-5_18}
}