C. Baier
等人理论计算机科学电子笔记
153
(
2006
)
97
定义2.1(马尔可夫决策过程(MDP),例如[20])MDP是
一
个集合
M
=
(
S
,
Act
,
P
,
sit
,
AP
,
L
)
,
其中
S
是
状态
的
有限集合,
Ac是
动作的有限集
合,P:(
S×
Act
×S
)
→
[0
,
1]是(三维)概率
矩阵
,
sit
∈
S
是
初始
状态,
AP
是一个拓扑
概率的有限集合,
L:S→2
AP
是一个标记函数。 Act(s)表示在状
态
s
中启用的动作集合,即动作集
α∈
Act使得P(
s
,
α
,
t
)
>
0
对于某个状态t∈S. 对于任何状态s∈S,我们要求Act(s)
对于任意一个
α
∈
Ac t
(
s
),
ε
SJ
∈
SP
(
s
,
α
,
SJ
)
=
1
.
(具体
来说
,
我们
认为
,
M
没有终端状态。)
Q
MDP的直观操作行为如下。如果
s
是当前状态,则第一个动作
α∈
Act(
s
)是
非确定性选择然后,执行动作α,以概率P(s
,
α
,
t)导致状态t
如果P(s
,
α
,
t)>0,我们称t为s
的
α-后继。动作α被称为
概率动作
,如
果它有一个随机效应,即,如果存在至少一个状态s,其中α被启用并且具有
两个或更多
个
α后继者。否则,α被称为非概率的。特别地,如果Act中的所
有动作都是非概率的,那么我们的MDP概念就简化为一个普通的转移系
统,每个状态和动作α至多有一个传出α-转移。当对现实系统建模时,大多
数动作α将是非概率的,因为它们产生唯一的后继状态。
道路。
MDP中的无限路径是序列n = s
0
,
α
1
,
s
1
,
α
2
,
. ∈(S×Act)
ω
使得
α
i
∈
Act(
s
i
−
1
)且P(
s
i
−
1
,
α
i
,
s
i
)
>
0,对任意
i≥
1。我们把路径写成
那么first(s)=
s
0
表示开始状态,trace(s)= L(s
0
)
,
L(s
1
)
,
L(s
2
)
,
. 字母
表2
AP
上的单词,通过
将字母
A投影到状态标签上获得。有限路径(用希腊字母σ
表示)是无穷的有限前缀。
nite路径结束于一个状态。我们使用符号first(
σ
)和trace(
σ
)作为无限路
径,last(
σ
)用于σ的最后状态,
|σ|
长度(动作数量)。
一群人。调度
器表示解决状态中的不确定性的实例,并且因此产生路径上的
马尔可夫链和概率度量。我们在这里考虑历史相关的、随机的随机数(简称
为随机数),它们由函数D给出,该函数D为任意有限路径σ分配Act(last
(
σ
))上的概率分布描述符对于PCTL的语义是必不可少的[2019 -01 -
22][2019- 01 - 22] 直觉上,调度器将计算的“历史”(由有限路径σ形式化)
作为输入,