Information Technology Reference
In-Depth Information
2.1 Stochastic Processes and Discrete-Time Markov Chains
The terminology introduced here follows that of Stewart [22]. A
stochastic process
with state space
S
and time domain
T
is a family of random variables
X
=
{
represents the outcome of observing
the state of the stochastic process at time
t
.
A
discrete-time Markov process
is a stochastic process where
T
is the non-
negative integers,
ZZ
∗
,and
X
t
|
t
∈
T
}
. A random variable
X
t
∈X
Pr[
X
n
+1
=
s
n
+1
|
X
0
=
s
0
,...,X
n
=
s
n
]=Pr[
X
n
+1
=
s
n
+1
|
X
n
=
s
n
]
)
ZZ
∗
and
s
i
∈
holds for all
n
S
. If the state space is discrete as well, then we
refer to the process as a
discrete-time Markov chain
. We will limit our attention
to discrete-time Markov chains. The techniques we present later on can be gen-
eralized to other types of stochastic processes, but it is beyond the scope of this
paper.
Let
p
ij
(
n
)=Pr[
X
n
+1
=
j
∈
X
n
=
i
], which denotes the probability of tran-
sitioning from state
i
at time
n
to state
j
at time
n
+1. We call
p
ij
(
n
), for all
i
and
j
in
S
and all
n
|
ZZ
∗
, the transition probabilities of the discrete-time
Markov chain. We have
p
ij
(
n
)
∈
S
,
j∈S
p
ij
(
n
)=1.If,
in addition to (1), we have
p
ij
(
n
)=
p
ij
(
m
) for all
n
and
m
in
ZZ
∗
, then the
discrete-time Markov chain is called
homogeneous
. In a homogeneous Markov
chain, transition probabilities are independent of time. The transition probabili-
ties of a finite-state homogeneous discrete-time Markov chain can be represented
by a single
∈
[0
,
1] and, for all
i
∈
transition probability matrix
P
. For notational convenience,
we will use
P
to represent the collection of transition probabilities,
p
ij
(
n
), for
nonhomogeneous Markov chains as well.
The evolution of a discrete-time Markov chain over time is captured by a
trajectory
. The trajectory of such a system is a sequence of states
σ
=
s
0
→
s
1
→···
|
S
|×|
S
|
S
.Wedenoteby
σ
[
i
]the
i
th state,
s
i
, along the trajectory
σ
, and the finite prefix of length
n
of
σ
is denoted
σ
,with
s
i
∈
n
.
Let
Path
(
s
) denote the set of trajectories with initial state
s
. Following Hans-
son and Jonsson [12], we define a probability measure
μ
on the set
Path
(
s
), for
each
s ∈ S
. The measure
μ
is defined on the probability space
↑
Ω,F
Ω
,where
Ω
=
Path
(
s
), and
F
Ω
is a
σ
-algebra generated by sets
{
σ
∈
Path
(
s
)
|
σ
↑
n
=
s
→
s
1
→···→
of trajectories with common finite prefix of length
n
.Themea-
sure
μ
can then be defined uniquely by induction on the length of the common
prefix as follows:
s
n
}
μ
(
{
σ
∈
Path
(
s
)
|
σ
↑
0=
s
}
)=1
(2)
μ
(
{
σ
∈
Path
(
s
)
|
σ
↑
n
=
s
→
s
1
→···→
s
n
}
)=
s
n−
1
}
·
p
s
n
−
1
s
n
(
n
−
μ
(
{
σ
∈
Path
(
s
)
|
σ
↑
(
n
−
1) =
s
→···→
)
1)
(3)
2.2
Temporal Stochastic Logic
We use the Probabilistic Computation Tree Logic (PCTL [12]) to specify prop-
erties of discrete-time Markov chains. We describe only a subset of PCTL that
Search WWH ::
Custom Search