key: cord-0048947-2mecxpx2 authors: Funke, Florian; Jantsch, Simon; Baier, Christel title: Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints date: 2020-03-13 journal: Tools and Algorithms for the Construction and Analysis of Systems DOI: 10.1007/978-3-030-45190-5_18 sha: 649d432c9701697e035605575a5ffb0908372763 doc_id: 48947 cord_uid: 2mecxpx2 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 [Formula: see text]-complete even for acyclic Markov chains. 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 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). Related work. The fundament of certifying algorithms has been surveyed in [64] . In the context of model checking, the most prominent approach for the certification of a positive result has been to construct a proof of the property in the system [15, 66, 67] . Rank-based certificates for the emptiness of a certain automaton [57] can be used to certify positive model checking results. Model checking MDPs in the presence of multiple objectives has been studied in [37, 39] . Heuristic approaches for computing small witnessing subsystems in DTMCs have been proposed in [5, 7, 49, 51, 52] and implemented in the tool Comics [50] . Witnessing subsystems in MDPs have been considered in [6, 9] and [19] , which focuses on succinctly representing witnessing schedulers. The mixed integer linear programming (MILP) formulation of [77, 78] allows for an exact computation of minimal witnessing subsystems for the property Pr max s0 (♦ goal) λ. NPcompleteness of computing minimal witnessing subsystems in MDPs was shown in [24] , but the exact complexity has, to the best of our knowledge, not been determined for DTMCs (the problem was conjectured to be NP-complete in [77] ). Minimal probabilistic counterexamples given as sets of paths can be computed by reframing the problem as a k-shortest-path problem [44, 45] . Regular expressions have been considered to succinctly represent the set of paths in [33] , and extensions were proposed in [18, 76] . The tool Dipro [4] computes probabilistic counterexamples, and a translation of these to fault trees was given in [56] . Another, learning-based, approach [20] also enumerates paths and produces a witnessing subsystem as a byproduct. But none of these approaches considers state-based minimality. Probabilistic counterexamples can be used to automatically guide iterative and refinement-based model checking techniques [23-25, 27, 48, 53] . Farkas' Lemma is a well-known source of certificates for the (in)feasibility of tasks in combinatorial optimization, operations research, and economics, as presented in the detailed historical account given in [70, pp. 209-226] as well as [62, Chapter 2] and [30, 65, 75] . The lecture notes [71] contain a rich variety of applications of linear programming in general and Farkas' Lemma in particular. Polyhedra and Farkas' Lemma. Throughout the article we write the dot product of two vectors x, y ∈ R n as xy or x · y. A halfspace in R n is a set H = {v ∈ R n | a · v ≤ b} for some non-trivial a ∈ R n and b ∈ R. A polyhedron is the intersection of finitely many halfspaces, and a polytope is a bounded polyhedron. A face of a polyhedron P is a subset F ⊆ P of the form F = {x ∈ P | a · x = max{a · y | y ∈ P }} for some a ∈ R n . A vertex of P is a face consisting of only one point. Farkas' Lemma [38] is part of the fundament of polyhedra theory and linear programming. It provides a natural source of certificates showing the infeasibility of a given system of inequalites, or in other words, the emptiness of the polyhedron described by the system. We will use it in the following version. A finite path is a finite sequence π = s 0 α 0 s 1 α 1 ...s n with the same condition for all 0 ≤ i ≤ n − 1. In this case, we define last(π) = s n . Denote by Paths(M) and Paths fin (M) the set of infinite and finite paths in M. A discrete-time Markov chain (DTMC) is an MDP with a single action which is enabled at every state. If M is a DTMC, then Paths(M) carries a probability measure, where the associated σ-algebra is generated by the cylinder sets Cyl(τ ) = {π ∈ Paths(M) | π has prefix τ } of finite paths τ = s 0 s 1 ...s n in M with probability Pr(Cyl(τ )) = ι(s 0 ) · 0≤i 0}. A deterministic scheduler is a function S : Paths fin (M) → Act such that S(π) ∈ Act(last(π)) and a randomized scheduler is a function S : Paths fin (M) → Dist(Act) such that supp(S(π)) ⊆ Act(last(π)) for all π ∈ Paths fin (M). Given a deterministic (or randomized) scheduler S, a path π = s 0 α 0 We denote by Pr S the probability measure on infinite S-paths (see [13, Definition 10 .92 on page 843] for more details). If we replace ι with the distribution concentrated on state s, then we obtain a probability measure Pr S M,s or short Pr S s on infinite S-paths starting in s. The scheduler is memoryless if S(π) = S(last(π)) for all π ∈ Paths fin (M). We abbreviate memoryless deterministic schedulers as MD-schedulers and memoryless randomized schedulers as MR-schedulers. Given a state t ∈ S, we let denote the maximal and minimal probability to reach t eventually when starting in s and set Pr min (♦t) = (Pr min s (♦t)) s∈S and Pr max (♦t) = (Pr max s (♦t)) s∈S . The supremum and infimum is indeed attained by an MD-scheduler [13, Lemmata 10.102 and 10.113], thus justifying the superscripts. Setting 2.2. Henceforth we will assume that M = (S all , Act, ι, P) has a unique initial state s 0 ∈ S and two distinguished absorbing states fail and goal ∈ S all , i.e., P(goal, α, s) = 0 for all α ∈ Act and s ∈ S all with s = goal, and likewise for fail. Here goal represents a desirable outcome of the modeled system and fail an outcome that is to be avoided. We use the notation S = S all \ {fail, goal}, we assume that every state s ∈ S is reachable from s 0 . We also assume that under every scheduler fail or goal is reachable from any state, i.e., Pr min s (♦(goal ∨ fail)) > 0 for all s ∈ S. If M does not satisfy this condition from the start, we can apply a standard preprocessing step, which is essentially given by taking the MEC quotient of M, see [2, 3] and also [26] . While it is often easier to verify the condition Pr min s (♦(goal ∨ fail)) > 0, it is in fact equivalent to Pr min s (♦(goal ∨ fail)) = 1 (see the full version [42] ). Whenever suitable, we denote by M also the set of enabled state-action pairs, We denote by b = (b(s, α)) (s,α)∈M ∈ R M with b(s, α) = P(s, α, goal) and by δ s0 the probability distribution that assigns 1 to s 0 , and 0 to all other states. The vectors Pr min (♦ goal) and Pr max (♦ goal) can be characterized using the following linear programs. Although this characterization is well-known, we give a proof in the full version [42] due to slight differences with the standard literature. In this section we establish certificates for the following statements: (1) All schedulers S satisfy Pr S s0 (♦ goal) λ (i.e., Pr min s0 (♦ goal) λ). Some scheduler S satisfies Pr S s0 (♦ goal) λ (i.e., Pr min s0 (♦ goal) λ). where ∈ {≤, <} and ∈ {≥, >}. The basis of our construction is the LP characterization of the probabilities above and, crucially, Farkas' Lemma. Certificates for universally-quantified statements. In order to deal with the cases (1) and (3), we need the following lemma proved in the full version [42] . Proof. For the direction from left to right, we take z to be Pr min (♦ goal). The opposite direction follows from Lemma 3.1. The right hand sides of Corollary 3.2 provide certifying formulations for problems (1) and (3): to check whether the corresponding threshold statement holds, one must merely check whether z satisfies the inequalities, rather than checking whether Pr min / max s0 (♦ goal) was computed correctly. If the threshold condition is satisfied, then the vectors Pr min / max s0 (♦ goal) are also valid certificates. Certificates for existentially-quantified statements. To find certificates for the cases (2) and (4), we calculate: For non-strict inequalities, we apply Farkas' Lemma in the opposite direction: The deductions for Pr max (♦ goal) are analogous, so that we get: In this section we consider the following problem: Given an MDP M that satisfies the property Pr min , find a small subsystem M of M that still satisfies these thresholds. Such a subsystem is a witness to the satisfaction of the property in M. We first define subsystems and consider different measures of size which we show to be equivalent. Then we deal with the question of finding minimal witnessing subsystems. Subsystems, witnesses and notions of minimality. Our definition of subsystem is essentially the same to the definition in [77, 78] Depending on the situation, one notion might be more suitable than the others. However, in the full version [42] we show that finding transition-minimal (respectively, size-minimal) witnesses can be reduced to finding state-minimal witnesses with a linear (respectively, quadratic) blow-up. We will therefore restrict ourselves to state-minimality for the rest of this paper. NP-completeness of finding minimal witnesses for DTMCs. In this section we determine the computational complexity of the witness problem: Given a DTMC M, a positive integer k, and a rational number λ ∈ [0, 1], decide whether there exists a witness M ⊆ M for Pr M,s0 (♦ goal) ≥ λ with at most k states. The corresponding problem for MDPs is known to be NPcomplete [24, 78] 1 . In this section we show that the witness problem is already NP-complete for acyclic DTMCs, where acyclicity means that the underlying graph with V = S and E = {(s, t) ∈ S × S | P(s, t) > 0} is acyclic (as before, we take S = S all \{goal, fail}). This answers a conjecture of [77] in the affirmative and also shows NP-completeness of finding minimal witnesses for Pr min M,s0 (♦ goal) ≥ λ. Theorem 4.5. The witness problem is NP-complete for acyclic DTMCs. Proof (Sketch). An NP-algorithm for the witness problem is given by guessing a set of states of size k and verifying in polynomial time that the corresponding subsystem satisfies Pr M ,s0 (♦ goal) ≥ λ. For hardness, we give a reduction from the clique problem, which is among Karp's 21 NP-complete problems [54] . The idea is the following: Given an instance of the clique problem with graph G = (V, E) and integer k, construct an acyclic Markov chain M with states S = {s 0 } ∪ V ∪ E ∪ {goal, fail} and edges from each vertex v ∈ V to all edges to which it is incident. Then the existence of a k-clique can be reduced to the existence of a "saturated" subsystem in M with k states in V . To check whether the subsystem is saturated, we require it to have more probability than a certain threshold, which depends on k and |V |. Details can be found in the full version [42] . Remark 4.6. NP-completeness of transition-minimal and size-minimal versions of the witness problem for acyclic DTMCs follows along the same lines, where only the sizes and thresholds for the subsystems need to be adapted. However, DTMCs whose underlying graph is a tree permit an efficient algorithm for computing minimal witnesses (for the proof see the full version [42] ). Proof (Sketch). The algorithm first transforms the DTMC at hand into a binary (tree-shaped) DTMC, and then works bottom up by storing for each state the highest probability that can be obtained with a subsystem of size k, for all k up to the size of the subtree. In this section we establish a strong connection between Farkas certificates on the one hand and witnesses for probabilistic reachability constraints on the other hand. We first note that the set of Farkas certificates for non-strict lower bounds forms a polytope, i.e., a bounded polyhedron. are both polytopes, called the polytopes of Farkas certificates. Remark 5.2. For any vector v ∈ R n the support is defined as supp(v) = {i ∈ {1, ..., n} | v i > 0}, and analogously for the vector spaces R S and R M . As our connection between subsystems of M and points in P min (λ) is based on taking the support, we restrict our attention to the subpolytope P min ≥0 (λ) = P min (λ) ∩ R S ≥0 . Notation 5.3. Given an MDP M = (S all , Act, s 0 , P) as in Setting 2.2 and a subset R ⊆ M, where M also denotes the state-action pairs (compare with Section 2). We let M R = (S all , Act, s 0 , P ) be the subsystem where, roughly speaking, the state-action pairs in R remain. More precisely, let if (s, α) / ∈ R, α ∈ Act(s) and t = fail 0 else (1) The subsystem M R is a witness for Pr min M,s0 (♦ goal) ≥ λ. (2) There is a point p in P min ≥0 (λ) such that supp(p) ⊆ R. Moreover, for a set R ⊆ M the following statements are equivalent: (a) The subsystem M R is a witness for Pr max M,s0 (♦ goal) ≥ λ. (b) There is a point p in P max (λ) such that supp(p) ⊆ R. (c) There is a vertex v of P max (λ) such that supp(v) ⊆ R. One consequence of Theorem 5.4 is that every MD-scheduler S with Pr S s0 (♦ goal) ≥ λ corresponds to a point in P max (λ), i.e. to a certificate for Pr max M,s0 (♦ goal) ≥ λ. (1) M supp(v) = (S all , Act, s 0 , P ) is a minimal witness for Pr max s0 (♦ goal) ≥ λ, (2) for every s ∈ S there is precisely one α ∈ Act(s) with (s, α) ∈ supp(v), In this section we use the results of Section 5 to derive two algorithms for the computation of minimal witnesses for reachability constraints in MDPs. As the problem is NP-hard, we also present a heuristic approach aimed at computing small witnessing subsystems. Vertex enumeration. Corollary 5.5 gives rise to the following approach of computing minimal witnessing subsystems: enumerate all vertices in the corresponding polytope and choose one with a maximal amount of zeros. Vertex enumeration of polytopes has been studied extensively [11, 12, 14, 21, 22, 35, 36, 40, 41, 63, 68] and has been shown to be computationally hard [55, Corollary 2] . First experiments that we have conducted with the SageMath 2 toolkit which supports vertex enumeration have not scaled well in the dimension, which in our case is the number of states in the original system. Also, we found no tool support for vertex enumeration that is able to handle sparse matrices, which is essential for bigger benchmarks. Mixed integer linear programming. An approach that computes minimal witnesses to the threshold problem Pr max s0 (♦ goal) ≥ λ using mixed integer linear programs (MILP) was presented in [77, 78] . Using the following lemma, we can derive MILP formulations from our polytope formulations. be a polytope and K ≥ 0 be such that for all p ∈ P and 1 ≤ i ≤ n we have p(i) ≤ K. Consider the MILP Then a vector (σ, x) is an optimal solution of this MILP if and only if x is a point in P with a maximal number of zeros. For P min ≥0 (λ) we can use Lemma 3.1 to derive that K = 1 is a viable bound. By invoking again Corollary 5.5, this means that a solution (z, σ) of the MILP encodes a minimal witnessing subsystem in the integral variables σ. This MILP was used in [77, 78] for the computation of minimal witnessing subsystems of DTMCs . An upper bound K as in Lemma 6.1 for P max (λ) can be found in polynomial time by taking the objective value of an optimal solution to the LP max (s,α)∈M y(s, α) s.t. y ∈ P max (λ) Remark 6.2. To compute minimal witnesses for Pr max s0 (♦ goal) ≥ λ, [77, 78] (witnesses for Pr min s0 (♦ goal) ≥ λ were not considered) propose the MILP with objective: min (s,α)∈M σ(s, α), subject to the conditions where σ(s, α) are binary integer variables. It was implemented in the tool ltlsubsys. The idea is to directly encode a scheduler in the set of equations Az ≤ b using σ. In [77, 78] a number of additional redundant constraints are given to guide the search. In contrast to [77, 78] we do not need to handle so-called problematic states, as our precondition Pr min s (♦(goal ∨ fail)) > 0 guarantees that no such states exist. k-step quotient sum (QS k ) heuristics. Approximating the maximal number of zeros in a polytope is computationally hard in general [8] . We now derive a heuristic approach for this problem called quotient sum heuristic which is based on iteratively solving LPs over the polytope, where the objective function for each iteration depends on an optimal solution of the previous LP. More precisely, we take o 1 = (1, . . . , 1) and take an optimal solution QS 1 of the LP min o 1 · y s.t. y ∈ P max (λ). Many entries in QS 1 may be small, but still greater than zero. In order to push as many of the small values of QS 1 to zero, we define a new objective function by where C is a value that is greater than any value 1/ QS 1 (i). We now take a solution QS 2 of the new LP min o 2 · y s.t. y ∈ P max (λ) and form the next objective function o 3 as in (6.3). Inductively this generates a sequence of objective functions (o k ) k≥1 and corresponding optimal solutions (QS k ) k≥1 in P max / min (λ). By Theorem 5.4 we can construct a witnessing subsystem with as many states as the number of non-zero entries in QS k . In this section we evaluate our MILP formulations and heuristics on a number of DTMC and MDP benchmarks from the Prism benchmark-suite [58, 59] . We compare our results with the tool Comics [50] , which implements heuristic approaches to compute small subsystems for DTMCs. It has two modes: the local search extends a given subsystem by short paths that carry much probability, whereas the global search searches for the next most probable path from the initial state to goal, and adds it to the subsystem. Both approaches iteratively extend a subsystem until it carries more probability than the given threshold and thus have to compute the probability of the subsystem at each iteration. All computations were performed on a computer with two Intel E5-2680 8 cores at 2.70 GHz running Linux, with a time bound of 30 minutes, a memory bound of 100 GB and with each benchmark instance having access to 4 cores. For the LP and MILP instances we use the Gurobi solver, version 8.1.1 [43] . The recorded times of our computations include the construction of the LPs/MILPs and are wall clock times. Pre-processing steps, such as collapsing states that cannot reach goal, are not counted in the time consumption. For Comics, we use the time that is reported as counterexample generation time by the tool. To validate our implementation, we used Prism to verify that the subsystems that we compute indeed satisfy the probability thresholds. We noticed that for a few instances (< 0.5%) Prism reported a deviation of less than 10 −8 , which can be explained by the fact that both Prism and the solvers that we use rely on floating-point arithmetic, which is approximate by nature. Our implementation, together with the models we use and benchmark results can be found at https://github.com/simonjantsch/farkas. DTMC benchmarks. As Pr max and Pr min coincide on DTMCs, we can use the heuristics and exact computations derived from either the P max or the P min ≥0 polytope for DTMCs (in Comics we use the standard query Pr s0 (♦ goal) ≥ λ). We consider two DTMC benchmarks: a model of the crowds-N -K protocol [69, 72] for ensuring anonymous web browsing (with N members and K protocol runs) and a model of the bounded retransmission protocol [34, 47] for file transfers (where brp-N -K is the instance with N chunks and K retransmissions). Figure 2 shows the effect of increasing the number of iterations of the QSheuristic for the model crowds-2-8. While the first iteration (taking QS 2 instead of QS 1 ) has an impact on the number of states, more iterations do not improve the result significantly. For QS 1 , the sizes of subsystems increase monotonically with growing λ. Starting with QS 2 the results may, interestingly, have "spikes": increasing λ can lead to smaller subsystems. Figure 3 shows the results of the QS 2 -heuristic compared to the two modes of Comics for λ that ranges between 0 and the actual reachability probability of the model. A general observation is that the runtime of the QS-heuristic is independent of λ, whereas both modes of Comics use significantly more time with increasing λ. The same observation can be done for memory consumption, which stayed below 200 MB for our heuristics. Also, especially for crowds-5-8, one can see that relatively small subsystems are possible even for large λ. The exact computations via MILPs hit the timeout for almost all instances. In Figure 3 it can be seen that the QS heuristics derived from the two polytopes P max and P min ≥0 may produce different results. However, for both models one of them gives monotonically growing subsystems and outperforms Comics. While QS 2 applied to P min ≥0 performs better on crowds-5-8 (Figure 3a) , it is the other way around on brp-512-2 ( Figure 3b ). In future work we intend to investigate what properties determine which of the two formulations performs better for a given DTMC. MDP benchmarks. We consider two MDP models: the randomized consensus-N -K protocol of [10, 60] (with N processes and a bound K on the random walk) and the CSMA-N -K protocol for data channels [61] (where N is the number of stations, and K is the maximal backoff count). The results of both heuristic and exact computations can be seen in Figure 4 and Figure 5 . Whereas the heuristics all needed less than 5 minutes, all MILP instances ran into the timeout except for the ones in Figure 4a . Whenever a MILP instance could not be solved optimally in 30 minutes, we plot both the found upper and lower bound, with the region in between shaded. It should be noted that the condition Pr min (♦(goal ∨ fail)) holds for the instances of these models, and reachability properties, that we consider. The comparison between the MILP formulation that we derived from P max (λ) and the one presented in [77, 78] (labeled by ltlsubsys, see also Section 6) shows that both compute comparable upper and lower bounds in Figure 4b , whereas ltlsubsys found worse upper bounds in Figure 5b . In all instances apart from Figure 4b the corresponding QS 2 heuristics performs well and generates subsystems that are as good, or better, than the best upper bounds computed by the MILPs in 30 minutes. As expected, the witnessing subsystems for Pr min s0 (♦ goal) ≥ λ tend to the entire state space as λ tends to the actual value Pr min s0 (♦ goal) (which is 1 in these two models). However, subsystems for Pr max s0 (♦ goal) ≥ λ may be substantially smaller even for large λ. In this paper we brought together two a priori unrelated notions in the context of probabilistic reachability constraints: on the one hand Farkas certificates, which are vectors satisfying certain linear inequalities that we derive using MDP-specific variants of Farkas' Lemma, and on the other hand witnessing subsystems, which provide insight into which parts of the system are essential for the satisfaction of the considered property. This connection reduces the computation of minimal (respectively, small) witnessing subsystems to finding a Farkas certificate with a maximal (respectively, large) number of zeros. Furthermore, it leads to a unified notion of witnessing subsystem for Pr max s0 (♦ goal) ≥ λ and Pr min s0 (♦ goal) ≥ λ. We showed that the decision version of computing minimal witnessing subsystems is NP-complete for acyclic DTMCs and introduced heuristics for the computation of small witnesses based on Farkas certificates. Experiments of the heuristics exhibited competitive results compared to the approach implemented in Comics and showed that they scale well with the system size and threshold. As expected, computing minimal subsystems using the derived MILP formulations consumed significantly more time than the heuristics and often triggered timeouts. The upper and lower bounds that were computed in the given time by the new MILP formulation for Pr max s0 (♦ goal) ≥ λ were comparable to known techniques. We have considered MDPs in which the probability to reach goal or fail is positive under each scheduler. In future work, we plan to extend our techniques to weaken this assumption. Exploring how vertex enumeration techniques could be adapted to the MDP-specific form of the Farkas polytopes is another interesting line of future work. We also plan to implement a tool for working with Farkas certificates in practice, which encompasses their generation as well as their independent validation. Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. Counterexample generation for discrete-time Markov models: An introductory survey Formal verification of probabilistic systems Temporal logics for the specification of performance and reliability Dipro -A tool for probabilistic counterexample generation Extended directed search for probabilistic timed reachability Generation of counterexamples for model checking of Markov decision processes Directed explicit state-space search in the generation of counterexamples for stochastic model checking On the approximability of minimizing nonzero variables or unsatisfied relations in linear systems Significant diagnostic counterexamples in probabilistic model checking Fast randomized consensus using shared memory A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra Reverse search for enumeration Principles of Model Checking (Representation and Mind Series An algorithm for finding all vertices of convex polyhedral sets From model checking to a temporal proof for partial models Model checking of probabilistic and nondeterministic systems Designing programs that check their work Counterexample generation for Markov chains using SMT-based bounded model checking Counterexample explanation by learning small strategies in Markov decision processes Verification of Markov Decision Processes Using Learning Algorithms Primal-dual methods for vertex and facet enumeration The vertex set of a 0/1 polytope is strongly P-enumerable Counterexample-driven synthesis for probabilistic program sketches A counterexample-guided abstraction-refinement framework for Markov decision processes CEGAR for qualitative analysis of probabilistic systems Reduction techniques for model checking Markov decision processes Counterexample-guided abstraction refinement for symbolic model checking Tree-like counterexamples in model checking Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday Linear invariant generation using non-linear constraint solving Verifying temporal properties of finite-state probabilistic programs The complexity of probabilistic verification Regular expressions for PCTL counterexamples Reachability analysis of probabilistic systems by successive refinements The complexity of vertex enumeration methods An algorithm for determining all extreme points of a convex polytope Multi-Objective Model Checking of Markov Decision Processes Theorie der einfachen ungleichungen Quantitative multi-objective verification for probabilistic systems Analysis of backtrack algorithms for listing all vertices and all faces of a convex polyhedron Double description method revisited Farkas certificates and minimal witnesses for probabilistic reachability constraints Gurobi optimizer reference manual Counterexamples in probabilistic model checking Counterexample generation in probabilistic model checking Termination of probabilistic concurrent program Proof-checking a data link protocol Probabilistic CEGAR Hierarchical counterexamples for discrete-time Markov chains The COMICS tool -computing minimal counterexamples for dtmcs Symbolic counterexample generation for discrete-time Markov chains Symbolic counterexample generation for large discrete-time Markov chains Shepherding hordes of Markov chains Reducibility among combinatorial problems Generating all vertices of a polyhedron is hard From probabilistic counterexamples via causality to fault trees From complementation to certification PRISM 4.0: Verification of probabilistic real-time systems The PRISM benchmark suite Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM Symbolic model checking for probabilistic timed automata Nonlinear Programming An algorithm for determining irrelevant constraints and all vertices in systems of linear inequalities Certifying algorithms Arbitrage and geometry Certifying model checkers From falsification to verification Efficient enumeration of the vertices of polyhedra associated with network LP's Crowds: Anonymity for web transactions Theory of Linear and Integer Programming A course in combinatorial optimization Probabilistic analysis of an anonymity system Automatic verification of probabilistic concurrent finite state programs An automata-theoretic approach to automatic program verification (preliminary report) The ubiquitous farkas lemma Counterexample generation for discrete-time Markov chains using bounded model checking Minimal critical subsystems for discrete-time markov models Minimal counterexamples for linear-time probabilistic verification