Farkas certificates and minimal witnesses for
probabilistic reachability constraints
Florian Funke , Simon Jantsch , and Christel Baier
Technische Universit¨ at Dresden, Germany
{florian.funke, simon.jantsch, christel.baier}@tu-dresden.de
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.
1 Introduction
The goal of program verification is to consolidate the user’s trust that a given
system works as intended, and if this is not the case, to provide her with useful
diagnostic information. Verification tools may, however, contain bugs and so a last
grain of insecurity regarding their results always remains. A widely acknowledged
approach to overcome this dilemma has been made in the form of certifying
algorithms [17, 64]. These algorithms provide every result with an accompanying
certificate, i.e., a token that can be used to verify the result independently and
with little ressources. In this way, certificates enable the user (or a third party)
to quickly give a mathematically rigorous proof for the correctness of the result
irrespective of whether the algorithm itself works correctly.
Counterexamples, i.e. certificates for the violation of a property, can often be
obtained as a byproduct of verification procedures. What constitutes a counterexample is highly context-dependent. Finite executions suffice as counterexamples
for safety properties and single, possibly infinite, executions are viable counterexamples for LTL [29]. Tree-like counterexamples have been considered for
This work was funded by DFG grant 389792660 as part of TRR 248, the Cluster of
Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence
Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training
Group QuantLA (GRK 1763).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 324–345, 2020.
https://doi.org/10.1007/978-3-030-45190-5 18
probabilistic reachability constraints
Florian Funke , Simon Jantsch , and Christel Baier
Technische Universit¨ at Dresden, Germany
{florian.funke, simon.jantsch, christel.baier}@tu-dresden.de
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.
1 Introduction
The goal of program verification is to consolidate the user’s trust that a given
system works as intended, and if this is not the case, to provide her with useful
diagnostic information. Verification tools may, however, contain bugs and so a last
grain of insecurity regarding their results always remains. A widely acknowledged
approach to overcome this dilemma has been made in the form of certifying
algorithms [17, 64]. These algorithms provide every result with an accompanying
certificate, i.e., a token that can be used to verify the result independently and
with little ressources. In this way, certificates enable the user (or a third party)
to quickly give a mathematically rigorous proof for the correctness of the result
irrespective of whether the algorithm itself works correctly.
Counterexamples, i.e. certificates for the violation of a property, can often be
obtained as a byproduct of verification procedures. What constitutes a counterexample is highly context-dependent. Finite executions suffice as counterexamples
for safety properties and single, possibly infinite, executions are viable counterexamples for LTL [29]. Tree-like counterexamples have been considered for
This work was funded by DFG grant 389792660 as part of TRR 248, the Cluster of
Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence
Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training
Group QuantLA (GRK 1763).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 324–345, 2020.
https://doi.org/10.1007/978-3-030-45190-5 18