1.一种对历史事务的建模验证方法，其特征在于，包括以下步骤：

步骤一：将系统建立模型表示为M＝(S,→,L)，其中S是一个状态集合，迁移关系→表示对每个s∈S，有某个s'∈S，满足s→s'，标记函数L表示S→P(Atoms)，P(Atoms)表示原子命题Atoms的幂集；

步骤二：对历史事务进行建模：

(1)增加一个计算过去一个政策被满足次数的量词，并用该量词来写另一个政策，公式扩展为Nx: 形式的构造，其中x绑定公式 并且不是自由出现的，表达方式如下：其中n＝|{j|1≤j≤iΛ(h,j)|＝ψ}|，h代表“历史事务”，i是一个整型变量，代表历史事务中的第i个会话，ψ是一个公式，Nx: 表示公式被满足的次数，iff表示当且仅当；

(2)设置一个量词进行筛选，用扩展的筛选量词来修正，其表达方式如下：其中 是筛选量词，保证对有限的值进行量化，是它的唯一的自由变量；

步骤三：用φ表示上述逻辑公式，为公式φ构造一个自动机，用Aφ表示，该自动机有一个接受迹的概念，迹是命题原子的赋值序列，从一条路径出发，可以抽象出它的迹，自动机Aφ有性质：编码满足φ的所有迹，即所有满足φ的迹；

步骤四：将自动机Aφ与模型M结合，结合运算的结果是一个迁移系统，其路径既是自动机的路径又是该迁移系统的路径；

步骤五：在结合的迁移系统中搜寻从s出发的满足逻辑公式φ；如果存在该路径，则输出“Yes,M,s|＝φ”，即存在相应的历史事务；如果没有这样的路径，则输出“No，M,s|≠φ”，即不存在相应的历史事务。

2.如权利要求1所述的对历史事务的建模验证方法，其特征在于，所述步骤二进一步包括：在一些历史数据无法获取或者丢失的情况，局部可观测性存在两个问题，一个是潜在可满足性，一个是遵守问题；部分可观察的会话是p(u1，...，un)形式的有限谓词集合，其中p是未解释的谓词符号，每个ui是常数或变量；部分可观察的历史是部分可观察会话的有限列表，在部分可观察历史中，用V(h)表示在历史h中出现的变量，用V(ψ)表示在公式ψ中出现的自由变量的集合。

3.如权利要求1所述的对历史事务的建模验证方法，其特征在于，所述步骤二中筛选量词 是对策略线性时序逻辑的直接扩展，即：if(h,i)|＝ψ(c1,...,cn)then(h,i)|＝φ[x1:＝c1,...,xn:＝cn]筛选量词产生公式的表达方式如下：

其中列表 是变量和常量的集合，用 表示只有唯一自由变量 的筛选量词，正项筛选量词 代表唯一的变量是 的公式，它的表达方式如下：其中，S表示“自从”操作符。