326
F. Funke et al.
Table 1: Overview of Farkas certificates for reachability properties in
MDPs (where ∈ {≤, <} and ∈ {≥, >}).
Property
Certificate dimension
Certificate condition
Pr
min
s0 (♦ goal) λ
z ∈ R
S
Az ≤ b ∧ z(s 0 ) λ
Pr
max
s0 (♦ goal) λ
y ∈ R
M
≥0
yA ≤ δ s0 ∧ yb λ
Pr
min
s0 (♦ goal) λ
y ∈ R
M
≥0
yA ≥ δ s0 ∧ yb λ
Pr
max
s0 (♦ goal) λ
z ∈ R
S
Az ≥ b ∧ z(s 0 ) λ
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.
2 Preliminaries
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
F. Funke et al.
Table 1: Overview of Farkas certificates for reachability properties in
MDPs (where ∈ {≤, <} and ∈ {≥, >}).
Property
Certificate dimension
Certificate condition
Pr
min
s0 (♦ goal) λ
z ∈ R
S
Az ≤ b ∧ z(s 0 ) λ
Pr
max
s0 (♦ goal) λ
y ∈ R
M
≥0
yA ≤ δ s0 ∧ yb λ
Pr
min
s0 (♦ goal) λ
y ∈ R
M
≥0
yA ≥ δ s0 ∧ yb λ
Pr
max
s0 (♦ goal) λ
z ∈ R
S
Az ≥ b ∧ z(s 0 ) λ
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.
2 Preliminaries
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