基于自动机的区间时序逻辑概率模型检测方法

技术领域

本发明属于计算机技术中的模型检测领域，具体地涉及到区间时序逻辑的概率模型检测。

背景技术

随着计算机软硬件及各种通信与安全技术的发展与成熟，人们验证各类大型系统运行的稳定性与可靠性的需求不断增加。模型检测是一种自动化验证方法，通过对待验证系统进行抽象与建模，再用时序逻辑公式对系统行为(一般称系统性质)进行描述，用验证算法判定系统的性质是否成立，从而验证系统的安全性和可靠性。区间时序逻辑是一种基于时间区间模型的时序逻辑，比一般基于时间点模型的逻辑语言有更丰富的行为描述能力，目前区间时序逻辑只应用在确定性系统中的定性验证，而随着近年对概率系统验证的需求增加，区间时序逻辑公式的概率定量验证仍没有较完善的方法。

针对现有的技术需求，本发明提出基于自动机的区间时序逻辑概率模型检测方法。

发明内容

本发明所解决的的技术问题在于克服上述现有技术的缺点，提供一种步骤简单、结果准确、容易实现的基于自动机的区间时序逻辑概率模型检测方法。

解决上述技术问题所采用的技术方案由下述步骤组成：

(1)构建离散时间马尔可夫链模型

按下式构建离散时间马尔可夫链模型D：

D＝(S

S

AP＝{a

P

L:S

其中，S

(2)构建系统Büchi自动机模型

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

(3)构建性质Büchi自动机模型

采用正则图方法构建性质Büchi自动机模型A

A

Q

I

T

F

其中，Q

(4)构建积自动机模型

按下式构建积自动机模型A

A

S

I

T

F

其中，S

(5)生成PRISM代码

将(4)步骤中的积自动机模型A

1)初始化状态变量为整型变量v，取值[0，N]，N为集合S

2)按下式得到变量v的状态迁移命令[]v：

Post(v

其中，v

3)按下式得到F

R＝P

其中，P

4)将1)、2)中得到的.pm格式模型代码文件导入模型检测器PRISM的model模块；

5)将3)中得到的.pctl格式公式代码文件导入模型检测器PRISM的property模块；

(6)输出概率定量结果

模型检测器PRISM返回概率定量结果，该结果为所述的系统性质在概率模型上成立的概率值p，范围值域为[0,1]。

本发明的(2)构建系统Büchi自动机模型步骤为：

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

本发明的(2)构建系统Büchi自动机模型步骤为：

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

本发明的(4)构建积自动机模型步骤为：

按下式构建积自动机模型A

A

S

I

T

F

其中，S

本发明的(4)构建积自动机模型步骤为：

按下式构建积自动机模型A

A

S

I

T

F

其中，S

由于本发明采用了Büchi自动机模型实现区间时序逻辑性质的概率模型检测，在离散时间马尔可夫链模型的基础上，通过构建系统Büchi自动机、性质Büchi自动机、积自动机、模型检测器PRISM代码，得到概率定量结果，简化了构建步骤，避免了复杂的计算过程。本发明具有步骤简单、容易实现、结果准确等优点，可以用于概率模型中安全性或活性等区间时序逻辑性质的概率定量结果检测。

附图说明

图1是本发明实施例1的流程图。

具体实施方式

下面结合附图和实例对本发明进一步详细说明，但本发明不限于下述的实施方式。

实施例1

本实施例的基于自动机的区间时序逻辑概率模型检测方法，由下述步骤组成(参见图1)：

(1)构建离散时间马尔可夫链模型

按下式构建离散时间马尔可夫链模型D：

D＝(S

S

AP＝{a

P

L:S

其中，S

(2)构建系统Büchi自动机模型

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

(3)构建性质Büchi自动机模型

采用正则图方法构建性质Büchi自动机模型A

A

Q

I

T

F

其中，Q

(4)构建积自动机模型

按下式构建积自动机模型A

A

S

I

T

F

其中，SP为状态集合，si为S

(5)生成PRISM代码

将(4)步骤中的积自动机模型A

1)初始化状态变量为整型变量v，取值[0，N]，N为集合S

2)按下式得到变量v的状态迁移命令[]v：

Post(v

其中，v

3)按下式得到F

R＝P

其中，P

4)将1)、2)中得到的.pm格式模型代码文件导入模型检测器PRISM的model模块。

5)将3)中得到的.pctl格式公式代码文件导入模型检测器PRISM的property模块。

(6)输出概率定量结果

模型检测器PRISM返回概率定量结果，该结果为所述的系统性质在概率模型上成立的概率值p，范围值域为[0,1]。

完成基于自动机的区间时序逻辑概率模型检测方法。

实施例2

本实施例的基于自动机的区间时序逻辑概率模型检测方法，由下述步骤组成：

(1)构建离散时间马尔可夫链模型

该步骤与实施例1相同。

(2)构建系统Büchi自动机模型

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

(3)构建性质Büchi自动机模型

该步骤与实施例1相同。

(4)构建积自动机模型

按下式构建积自动机模型A

A

S

I

T

F

其中，S

(5)生成PRISM代码

将(4)步骤中的积自动机模型A

1)初始化状态变量为整型变量v，取值[0，N]，N为集合S

2)按下式得到变量v的状态迁移命令[]v：

Post(v

其中，v

3)按下式得到F

R＝P

其中，P

4)将1)、2)中得到的.pm格式模型代码文件导入模型检测器PRISM的model模块。

5)将3)中得到的.pctl格式公式代码文件导入模型检测器PRISM的property模块。

其它步骤与实施例1相同。

完成基于自动机的区间时序逻辑概率模型检测方法。

实施例3

本实施例的基于自动机的区间时序逻辑概率模型检测方法，由下述步骤组成：

(1)构建离散时间马尔可夫链模型

该步骤与实施例1相同。

(2)构建系统Büchi自动机模型

按下式构建系统Büchi自动机模型A

A

S

I

F

∑＝2

T

其中，S

(3)构建性质Büchi自动机模型

该步骤与实施例1相同。

(4)构建积自动机模型

按下式构建积自动机模型A

A

S

I

T

F

其中，S

(5)生成PRISM代码

将(4)步骤中的积自动机模型A

1)初始化状态变量为整型变量v，取值[0，N]，N为集合S

2)按下式得到变量v的状态迁移命令[]v：

Post(v

其中，v

3)按下式得到F

R＝P

其中，P

4)将1)、2)中得到的.pm格式模型代码文件导入模型检测器PRISM的model模块。

5)将3)中得到的.pctl格式公式代码文件导入模型检测器PRISM的property模块。其它步骤与实施例1相同。

完成基于自动机的区间时序逻辑概率模型检测方法。