Page 84 - 《软件学报》2021年第7期

2002 Journal of Software 软件学报 Vol.32, No.7, July 2021

1 预备知识

1.1 朴素贝叶斯算法
朴素贝叶斯或简单贝叶斯分类器广泛应用于数据分析.朴素贝叶斯分类器 [19] ,基于关键的约束假设,即属性
X i 之间彼此独立,也就是 P(X i |X k )=P(X i ).
 (P 类别 ) (P 特征 1,特征 2, ,特征 N ) 
P  | 特征 1,特征 2, ,特征 N  .  类别
 ( P 特征 1,特征 2, ,特征 N ) 
上述公式是朴素贝叶斯分类器的原理,即在给定 n 个特征的情况下,计算事件属于某个类别的概率,概率
最大的那个类别即为该事件所属类别.虽然贝叶斯分类原理很简单,但却有着高效的学习效率和准确的分类效
果.原因是,我们不需要知道类别概率的精确值 P(1,2,...,k),只需要分类器对它们进行正确的分类.朴素贝叶斯
算法被广泛应用在机器学习中,相较于其他监督学习分类算法,其所需考虑的参数更少也更简单、高效.朴素贝
叶斯算法主要包括 3 个阶段:准备阶段、学习阶段和预测阶段.在准备阶段,需要进行数据预处理,指定特征属性
和类别,获取训练数据.在学习阶段,首先要估计每个类别出现的概率,估计每个类别下每个特征属性出现的概
率,然后对于每个属性组合,分别计算其归属于每个类别的概率.在预测阶段,针对输入的特征属性集合,挑选最
大概率所属的类别作为最终的分类结果.
1.2 随机混成自动机SHA
考虑到我们的模型中含有时间、速度等连续变量,信号灯表示属于离散变量.同时,驾驶员状态的迁移以及
行人对于来往车辆的关注行为都带有不确定的特性.因此,我们用随机混成自动机来构建模型.随机混成自动机
(stochastic hybrid automata,简称 SHA) [20] 是混成自动机带有随机行为的版本.用于实现对带有随机混成行为的
系统建模,即包含离散和连续变化的变量,同时状态之间迁移带有随机行为.本文关注的不确定环境下的人机物
系统包含混成行为和随机行为,且对时间约束高度敏感.因此,本文将无人驾驶系统特征映射到随机混成自动
机,实现自动化的模型验证.SHA 是对混成自动机 HA 进行了随机语义扩展,状态之间的迁移可基于离散概率分
布 [21] .
随机混成自动机是一个八元组 M=(L,l,C,Act,inv,enab,prob,F),其中,
 L 表示位置的有限集合;
 l 表示初始位置,lL;
 C 表示时钟的有限集合;
 Act 表示动作的有限集合;
 inv:LCC(C)表示不变式的有限集合,CC 表示时钟约束函数;
 enab:L×ActCC(C)表示迁移触发的条件;
C
 prob:L×ActDist(2 ×L)表示概率迁移函数;
 F:L→2 AP 表示将每个位置映射到原子命题集合的标签函数.
1.3 概率计算树逻辑PCTL

概率计算树逻辑(probabilistic computation tree logic,简称 PCTL)是对计算树逻辑(computation tree logic,简
称 CTL)的概率扩展,用概率运算符 P 定量扩展了 CTL 的路径量词“所有(all,简称 A)”和“存在(exists,简称 E)”.
PCTL 的详细语义参见文献[22,23].PCTL 语法的状态公式和路径公式的定义如下所示:
 :true ap      P  p ( ),
  U  {≤ k  } | X .
: 
其中,AP 表示原子命题集合,apAP,p[0,1],kN,⨝{≤,<,>,≥},时序操作符 X 表示 Next,U 表示 Until.状态
公式中的每个状态被评估为 true 或 false.状态 s 满足关系定义如下:
s | true, |s  ap iff ap inv ( )s