Farkas certificates and minimal witnesses
325
fragments of CTL [28]. For a probabilistic system M and a linear time property
φ, the most prominent notion of counterexample to Pr M (φ) < λ is a set of paths
satisfying φ whose probability mass is at least λ (see [1] for a survey).
Another notion of counterexample for probabilistic systems M and properties
of the form Pr M (φ) < λ are critical subsystems [1]. We adopt the reverse
perspective and call a subsystem M
of M a witnessing subsystem for the
property Pr M (φ) ≥ λ if Pr M (φ) ≥ λ. Small witnessing subsystems offer an
insight into what parts of the system are responsible for the satisfaction of the
property. Nonetheless, witnessing subsystems can hardly be regarded as viable
certificates since verifying Pr M (φ) ≥ λ is as hard as checking Pr M (φ) ≥ λ itself.
In this paper we build a solid bridge between certificates and witnessing
subsystems. The systems we consider are modeled as Markov decision processes
(MDP), which contain an absorbing goal state representing a desirable outcome.
This approach is motivated by the fact that numerous model checking tasks can
be reduced to reachability problems [3, 31, 32, 46, 73, 74].
Using Farkas’ Lemma, we introduce certificates for bounds on the minimal
and maximal probability to reach the goal state. We show that the set of these
certificates forms a polytope and we provide a direct translation of a certificate
to a witnessing subsystems for lower bounded threshold properties. Thereby, we
bridge the gap between an abstract gadget, serving solely as a proof that the
result is correct, and a concrete object, containing crucial diagnostic information
about why the result holds. Moreover, our translation reduces the computation
of minimal witnessing subsystems to a purely geometric problem, for which we
provide and evaluate new exact and heuristic algorithms.
All omitted proofs can be found in the full version of this paper [42].
Contributions.
– Following the concept of certificates in certifying algorithms, we introduce
Farkas certificates for reachability problems in MDPs (Table 1).
– We give a uniform notion of witnessing subsystem (WS) for Pr
max
s0 (♦ goal) ≥
λ and Pr
min
s0 (♦ goal) ≥ λ (Definition 4.1). To the best of our knowledge,
witnesses for Pr
min
s0 (♦ goal) ≥ λ have not been considered previously.
– We establish NP-completeness for finding minimal WS even for acyclic discrete
time Markov chains (DTMC) (Theorem 4.5).
– Our main result establishes a strong connection between the polytopes of
Farkas certificates for Pr
min
s0 (♦ goal) ≥ λ and Pr
max
s0 (♦ goal) ≥ λ and WS of
the same property (Theorem 5.4). In particular, one can read off a minimal WS
from a vertex of the polytope with a maximal number of zeros (Corollary 5.5).
– From our polytope characterizations we derive two algorithms for computing
minimal WS: one based on vertex enumeration and one based on mixed integer
linear programming (Section 6). We also introduce a linear programming
based heuristic aimed at computing small WS. We evaluate our approach
on DTMC and MDP benchmarks, where particularly our heuristics show
competitive results compared to state-of-the-art techniques (Section 7).
325
fragments of CTL [28]. For a probabilistic system M and a linear time property
φ, the most prominent notion of counterexample to Pr M (φ) < λ is a set of paths
satisfying φ whose probability mass is at least λ (see [1] for a survey).
Another notion of counterexample for probabilistic systems M and properties
of the form Pr M (φ) < λ are critical subsystems [1]. We adopt the reverse
perspective and call a subsystem M
of M a witnessing subsystem for the
property Pr M (φ) ≥ λ if Pr M (φ) ≥ λ. Small witnessing subsystems offer an
insight into what parts of the system are responsible for the satisfaction of the
property. Nonetheless, witnessing subsystems can hardly be regarded as viable
certificates since verifying Pr M (φ) ≥ λ is as hard as checking Pr M (φ) ≥ λ itself.
In this paper we build a solid bridge between certificates and witnessing
subsystems. The systems we consider are modeled as Markov decision processes
(MDP), which contain an absorbing goal state representing a desirable outcome.
This approach is motivated by the fact that numerous model checking tasks can
be reduced to reachability problems [3, 31, 32, 46, 73, 74].
Using Farkas’ Lemma, we introduce certificates for bounds on the minimal
and maximal probability to reach the goal state. We show that the set of these
certificates forms a polytope and we provide a direct translation of a certificate
to a witnessing subsystems for lower bounded threshold properties. Thereby, we
bridge the gap between an abstract gadget, serving solely as a proof that the
result is correct, and a concrete object, containing crucial diagnostic information
about why the result holds. Moreover, our translation reduces the computation
of minimal witnessing subsystems to a purely geometric problem, for which we
provide and evaluate new exact and heuristic algorithms.
All omitted proofs can be found in the full version of this paper [42].
Contributions.
– Following the concept of certificates in certifying algorithms, we introduce
Farkas certificates for reachability problems in MDPs (Table 1).
– We give a uniform notion of witnessing subsystem (WS) for Pr
max
s0 (♦ goal) ≥
λ and Pr
min
s0 (♦ goal) ≥ λ (Definition 4.1). To the best of our knowledge,
witnesses for Pr
min
s0 (♦ goal) ≥ λ have not been considered previously.
– We establish NP-completeness for finding minimal WS even for acyclic discrete
time Markov chains (DTMC) (Theorem 4.5).
– Our main result establishes a strong connection between the polytopes of
Farkas certificates for Pr
min
s0 (♦ goal) ≥ λ and Pr
max
s0 (♦ goal) ≥ λ and WS of
the same property (Theorem 5.4). In particular, one can read off a minimal WS
from a vertex of the polytope with a maximal number of zeros (Corollary 5.5).
– From our polytope characterizations we derive two algorithms for computing
minimal WS: one based on vertex enumeration and one based on mixed integer
linear programming (Section 6). We also introduce a linear programming
based heuristic aimed at computing small WS. We evaluate our approach
on DTMC and MDP benchmarks, where particularly our heuristics show
competitive results compared to state-of-the-art techniques (Section 7).