5 An Introduction to Imprecise Markov Chains
165
Definition 5.14 Let P be an IDTMC, and let T t be the associated family of sets of
transition matrices, as defined above. Then, for each t ∈ N 0 , the associated lower
transition operator T t : L (X ) → L (X ) is defined, for all f ∈ L (X ) and all
x ∈ X , as
T t f
(x) := inf
T t ∈T t
T t f
(x) .
This lower transition operator essentially fulfils the same role as the transition
matrices from which it is derived. In particular, we have the following:
Proposition 5.5 Let P be an IDTMC, and let T t be the associated family of lower
transition operators. Then, for all f ∈ L (X ), all t ∈ N 0 and all x ∈ X , it holds
that
T t f
(x) = E P
f (X t+1 ) | X t = x
.
Proof Simply use the definitions together with Proposition 5.3:
T t f
(x)= inf
T t ∈T t
T t f
(x)= inf
T t ∈T t
y∈X
f (y)T t (x, y)
=
inf
P (X t+1 |X t )∈P(X t+1 |X t )
y∈X
f (y)P (X t+1 =y|X t = x)
= inf
P ∈P
y∈X
f (y)P (X t+1 =y|X t =x)
= inf
P ∈P
E P
f (X t+1 )
X t =x
=E P
f (X t+1 )
X t =x
,
where in the fourth equality, we used the definition of the compatible measures.
As in Corollary 5.3, we can now state the simplified law of iterated lower
expectation for imprecise Markov chains, using these lower transition operators:
Theorem 5.3 Let P be an IDTMC that is separately specified, and let T t be the
associated family of lower transition operators. Then, for all f ∈ L (X ), all s, t ∈
N 0 such that s ≤ t and all x ∈ X , it holds that
E P
f (X t )
X s = x
=
T s · · · T t f
(x) ,
where the right-hand side represents an iterated operator product (composition).
We omit the full proof, but the interested reader can reconstruct the argument by
using the general computational process of iterated lower expectation as explained
in Sect. 5.3.1, the imprecise Markov property from Definition 5.10 and the
interpretation of the lower transition operator from Proposition 5.5.