Farkas certificates and minimal witnesses
327
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.
Lemma 2.1 (Farkas’ Lemma, cf. [70, Corollary 7.1f on p. 90]). Let
A ∈ R
m×n and b ∈ R
m . Then there exists z ∈ R
n
≥0 with Az ≤ b if and only if
there does not exist y ∈ R
m
≥0 with yA ≥ 0 ∧ yb < 0.
Markov decision processes. A Markov decision process (MDP) is a tuple
M = (S, Act, ι, P), where S is a finite set of states, Act is a finite set of actions,
ι is a probability distribution on S called the initial distribution of M , and
P : S × Act ×S → [0, 1] is the transition probability function where we require
s ∈S P(s, α, s
) ∈ {0, 1} for all s ∈ S and α ∈ Act. An action α is enabled in
state s ∈ S if
s ∈S P(s, α, s
) = 1. The set of enabled actions at state s are
denoted by Act(s), and we require Act(s) = ∅ for all s ∈ S. A path in an MDP
M is an infinite sequence s 0 α 0 s 1 α 1 ... such that P(s i , α i , s i+1 ) > 0 for all i ≥ 0.
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
probability distributions on X by Dist(X). Given μ ∈ Dist(X) let the support of
μ be supp(μ) = {x ∈ X | μ(x) > 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 s 1 α 1 ... in M is an
S-path if α i = S(s 0 α 0 ...s i ) (or α i ∈ supp(S(s 0 α 0 ...s i ))) for all i ≥ 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.
327
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.
Lemma 2.1 (Farkas’ Lemma, cf. [70, Corollary 7.1f on p. 90]). Let
A ∈ R
m×n and b ∈ R
m . Then there exists z ∈ R
n
≥0 with Az ≤ b if and only if
there does not exist y ∈ R
m
≥0 with yA ≥ 0 ∧ yb < 0.
Markov decision processes. A Markov decision process (MDP) is a tuple
M = (S, Act, ι, P), where S is a finite set of states, Act is a finite set of actions,
ι is a probability distribution on S called the initial distribution of M , and
P : S × Act ×S → [0, 1] is the transition probability function where we require
s ∈S P(s, α, s
) ∈ {0, 1} for all s ∈ S and α ∈ Act. An action α is enabled in
state s ∈ S if
s ∈S P(s, α, s
) = 1. The set of enabled actions at state s are
denoted by Act(s), and we require Act(s) = ∅ for all s ∈ S. A path in an MDP
M is an infinite sequence s 0 α 0 s 1 α 1 ... such that P(s i , α i , s i+1 ) > 0 for all i ≥ 0.
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
probability distributions on X by Dist(X). Given μ ∈ Dist(X) let the support of
μ be supp(μ) = {x ∈ X | μ(x) > 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 s 1 α 1 ... in M is an
S-path if α i = S(s 0 α 0 ...s i ) (or α i ∈ supp(S(s 0 α 0 ...s i ))) for all i ≥ 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.