面向cps的
μ
演算实数值性能评价方法
技术领域
1.本发明公开了一种面向cps的μ演算实数值性能评价方法，主要用于对cps使用形式化验证的方法进行系统验证，并通过输出为实数值的性能评价语言进行系统度量分析。
背景技术：2.信息物理融合系统(cps)是基于行为离散、时间连续的复杂混成系统，同时在实际应用中，还可能夹杂着不确定性、资源消耗性等各种附带信息的属性。这种混成系统在现实生活中受到了广泛的运用，而在受到人们广泛运用的同时，混成系统的安全性和可靠性也变得尤为重要。因此，保证这类混成系统的安全性和可靠性也成为了目前的主要研究方向。模型检测技术是一个基于有限状态的形式化验证技术，通过对系统进行形式化的建模，并采用可以描述形式化模型的相应逻辑语言来表达需要验证的性质，并将性质由公式的形式所表达出来，通过模型检测算法进行相应的验证。目前模型检测技术通常使用的经典模型有有限状态自动机、时间自动机、概率自动机、混成自动机以及进程代数csp(communication sequentialprocess)、ccs(calculus of communicating systems)等，经典时序逻辑有线性时序逻辑 ltl(linear temporal logic)和计算树逻辑ctl(computation tree logic)。
3.针对cps的不确定性和时间消耗性，经典的ltl和ctl时序逻辑语言没有足够的能力刻画相应的性质，因此有学者在前两者的基础上添加了概率算子和时间算子，提出了概率计算树逻辑pctl(probabilistic computation tree logic)、概率线性时序逻辑pltl(lineartemporal logic with probability)以及时间计算树逻辑tctl(timed computation treelogic)，并分别给出了模型检测算法。然而即使增加了时间或概率算子，能够刻画出相应的概率性质和时间性质，但仍然无法对具体的实数值进行刻画。换言之，传统的模型检测技术仅仅是对所要验证的一个性质公式进行形式化验证，而后得出相应的布尔值，即true或false，而并不能得到满足某个性质的条件下，会花费多少时间，或者以多大/小的概率能够满足该性质。为了解决这类传统的时序逻辑语言遇到的问题，本发明通过已有的性能评价语言ctml (computation tree measurement language)以及传统的μ演算提出了一个表达能力较强的的性能评价语言——μr。
技术实现要素：4.信息物理融合系统存在着不确定性且伴随资源消耗。由于传统的μ演算无法描述需要输出实数值的性质，而其表达能力却非常强大，因此本发明在其基础上，与性能评价方法相结合，将μ演算通过函数的方法转换至性能评价方法中。
5.本发明是一种面向cps的μ演算实数值性能评价方法，主要包括以下步骤：
6.步骤1：对kripke结构引入原子函数，有以下一个元组(af)
7.af是原子函数的有限集合，每一个状态都有与之相对应的原子函数，即该状态下原子命题满足时，其函数取值为1，否则为0。
8.步骤2：将μ演算的语义解释从状态集合推广至{0，1}的函数，其包含以下五个主要转换
9.(1)原子命题公式的语义解释转换；
10.(2)合取逻辑算子公式的语义解释转换；
11.(3)析取逻辑算子公式的语义解释转换；
12.(4)<a>算子公式的语义解释转换；
13.(5)[a]算子公式的语义解释转换。
[0014]
步骤3：将函数的值域从{0，1}扩展至实数值域r，并以此提出新的性能评价语言μr
[0015]
首先根据步骤2的转换将集合转换为函数，再将函数的值域从{0，1}扩展至整个实数域r。再根据这个函数提出相应的μr性能评价语言的语法和语义。
[0016]
步骤4：对μr性能评价语言中的语义解释环境进行偏序集证明、最大上界存在及完备格证明以及τ函数单调性证明
[0017]
根据μr性能评价语言中的语义环境，对τ函数的值域以及其计算方法进行相应的偏序集证明、完备格证明，再对整个τ函数进行单调性证明，最后通过tarski不动点定理证明μr 语言中提出的不动点的存在性，即μr语言的合理性。
[0018]
本发明根据信息物理融合系统的实际特性以及现有的性能评价语言对μ演算进行了扩展，使其能够足以描述信息物理融合系统的不确定性、资源消耗等性质的度量分析，同时使用 tarski不动点定理证明扩展后的语言的正确性，为后续进一步的形式化验证和分析工作奠定基础。
附图说明
[0019]
图1为面向cps的μ演算实数值性能评价方法的流程图
[0020]
图2为kripke结构例子
具体实施方式
[0021]
本发明的实施提供了一种面向cps的μ演算实数值性能评价方法，为使本领域技术人员更好地理解本发明的技术方案，下面结合附图和具体实施方式对本发明作进一步详细描述。通过参考附图描述的实施方式是示例性的，仅用于解释本发明，而不能解释为对本发明的限制。
[0022]
本发明的目的是，为了解决表达能力非常强大的μ演算无法对复杂的信息物理融合系统进行直接的性能评价的目的，针对其语义解释的集合性质，通过函数的方法将其输出值从布尔域扩展至实数域，并由此提出新的性能评价语言μr用来对cps的概率、权值等属性进行性能评估。
[0023]
面向cps的μ演算实数值性能评价方法的流程如附图1所示。具体的发明实施方法如下：
[0024]
1.从布尔域到实数域的扩展
[0025]
对于传统的模型检测技术和算法而言，性能评价语言与之最大的区别就是输入与输出的值域的不同。在传统的形式化验证方法中，
[0026]
通常使用布尔值(true或false)作为输出，来判断输入的公式是否为该系统满足
的属性；而在性能评价语言中，则将输出从布尔值推广到实数值，可以对整个系统在某个状态下满足某个公式所需要的度量值进行量化的计算，得出一个具体或近似的实数值来。本发明将把μ演算的输出值推广至实数域，使用kripke结构作为基本的迁移系统进行解释，并给出推广为实数域的语言μ
f
的语法和语义。
[0027]
在给出μ
f
的语法语义定义之前，先给出迁移系统的定义。本发明选取kripke结构作为基本的迁移系统进行后续的验证分析。kripke结构定义如下：
[0028]
定义5.1(kripke)kripke结构是一个五元组m＝(s，s0，ap，r，l)，其中：
[0029]
(1)s是一个有限状态集合；
[0030]
(2)s0是一个有限初始状态集合；
[0031]
(3)ap是原子命题的有限集合；
[0032]
(4)r是一个迁移关系，其中r是左总的，即
[0033]
(5)l是一个标签函数，s
→2ap
，表示每个状态s∈s满足的原子命题的集合l(s)。
[0034]
如图2所示，m＝(s，s0，ap，r，l)是一个具体的kripke结构，其中，
[0035]
(1)状态集s是{s1，s2，s3}；
[0036]
(2)初始状态集为{s1}；
[0037]
(3)原子命题集合是{p，q}；
[0038]
(4)迁移关系有{(s1，s2)，(s2，s3)，(s3，s1)，(s1，s3)}；
[0039]
(5)l(s1)＝{p}，l(s2)＝{p，q}，l(s3)＝{q}。
[0040]
2.μ演算从集合推广至函数
[0041]
本发明主要的研究内容是将形式化验证语言从布尔值推广至实数值，而对于μ演算而言，其语义是将系统中满足该公式的所有状态作为集合来输出，与经典的时序逻辑有所不同。因此，本发明先将其输出从集合推广为函数。
[0042]
传统的μ演算公式是一个满足性质的状态集合，我们可以把这个集合看作是一个从状态集合到{0，1}的函数f：s
→
{0，1}，其中每个状态都映射到0或1，当这个状态满足该性质时，该状态将映射到1，反之则映射为0。以上面的kripke结构m为例，对于每一种公式，如下给出相应的变换：
[0043]
(1)原子命题公式的语义解释转换[[p]]
m
e：
[0044]
公式p与公式q是原子命题，由kripke结构m可以得出：
[0045]
[[p]]em＝{s|p∈l(s)}＝{s1，s2}，
[0046]
[[q]]em＝{s|q∈l(s)}＝{s3，s2}，
[0047]
将集合{s1，s2}看作为函数f
p
：s
→
{0，1}，其中，f
p
(s1)＝1，f
p
(s2)＝1，f
p
(s3)＝0；
[0048]
将集合{s3，s2}看作为函数f
q
：s
→
{0，1}，其中，f
p
(s1)＝0，f
p
(s2)＝1，f
p
(s3)＝1；
[0049]
那么公式p的语义解释从集合变为函数f
p
，即[[p]]em＝f
p
，公式q的语义解释从集合变为函数f
q
，即[[q]]em＝f
q
；
[0050]
(2)合取逻辑算子公式的语义解释转换[[h]]em＝[[f∧g]]em：
[0051]
将原子命题公式p作为公式f，q作为公式g，那么根据(1)可知：
[0052]
[[f]]em＝[[p]]em＝{s1，s2}，
[0053]
[[g]]em＝[[q]]em＝{s3，s2}，
[0054]
[[h]]em＝[[f∧g]]em＝[[f]]em∩[[g]]em＝{s2}，
[0055]
将集合{s2}看作为函数f
h
：s
→
{0，1}，其中，f
h
(s1)＝0，f
h
(s2)＝1，f
h
(s3)＝0；
[0056]
那么公式h的语义解释从集合变为函数f
h
，即[[h]]em＝f
h
；
[0057]
而从函数的计算来看，则是对f
p
与f
q
的每一个状态所映射的值进行取最小值操作，即 f
h
＝min{f
p
，f
q
}。
[0058]
(3)析取逻辑算子公式的语义解释转换[[h]]em＝[[f∨g]]em：
[0059]
将原子命题公式p作为公式f，q作为公式g，那么根据(1)可知：
[0060]
[[f]]em＝[[p]]em＝{s1，s2}，
[0061]
[[g]]em＝[[q]]em＝{s3，s2}，
[0062]
[[h]]em＝[[f∨g]]em＝[[f]]em∪[[g]]em＝{s1，s2，s3}，
[0063]
将集合{s1，s2，s3}看作为函数f
h
：s
→
{0，1}，其中，f
h
(s1)＝1，f
h
(s2)＝1，f
h
(s3)＝1；
[0064]
那么公式h的语义解释从集合变为函数f
h
，即[[h]]em＝f
h
；
[0065]
而从函数的计算来看，则是对f
p
与f
q
的每一个状态所映射的值进行取最大值操作，即 f
h
＝max{f
p
，f
q
}。
[0066]
(4)<a>算子公式的语义解释转换[[k]]em＝[[<a>h]]em：
[0067]
将原子命题公式p作为公式f，q作为公式g，h为f∧g，那么根据(1)(2)可知：
[0068][0069]
将集合{s1}看作为函数f
k
：s
→
{0，1}，其中，f
k
(s1)＝1，f
k
(s2)＝0，f
k
(s3)＝0；
[0070]
那么公式k的语义解释从集合变为函数f
k
，即[[k]]em＝f
k
；
[0071]
而从函数的计算来看，则是对f
k
的每一个状态所映射的值进行取其所有后继状态在函数 f
h
上映射的值的最大值操作，即f
k
(s)＝max{f
f
(t1)，f
f
(t2)，f
f
(t3)，
…
}，其中t1，t2，t3为状态s 的后继状态。
[0072]
(5)[a]算子公式的语义解释转换[[k]]em＝[[[a]h]]em：
[0073]
将原子命题公式p作为公式f，q作为公式g，h为f∧g，那么根据(1)(2)可知：
[0074][0075]
将集合{s2，s3}看作为函数f
k
：s
→
{0，1}，其中，f
k
(s1)＝0，f
k
(s2)＝1，f
k
(s3)＝1；
[0076]
那么公式k的语义解释从集合变为函数f
k
，即[[k]]em＝f
k
；
[0077]
而从函数的计算来看，则是对f
k
的每一个状态所映射的值进行取其所有后继状态在函数 f
h
上映射的值的最小值操作，即f
k
(s)＝min{f
f
(t1)，f
f
(t2)，f
f
(t3)，
…
}，其中t1，t2，t3为状态s 的后继状态。
[0078]
由上述每一个算子从状态集合到状态函数的转换，将函数的值域从{0，1}扩展至[a，b]，其中a，b为非零实数，a＜b，那么就可以对相关性质度量进行实数计算。
[0079]
3.μ
f
语法和语义
[0080]
μ
f
的基本思想就是把映射的{0，1}集合扩展为实数值的一个闭区间[a，b]中，具体的a和b 的值由实际例子决定。状态映射函数f的定义如下：
[0081]
定义5.2(状态映射函数f)μ
f
语言的公式f是一个函数，表示从状态空间s到一个闭区间的映射：
[0082]
f：s
→
[a，b]
[0083]
在经典的kripke结构中，每个状态内都有一个或多个原子命题，这些原子命题通过标签函数l进行描述。而针对μ
f
语言，本发明对kripke结构进行了相应的改进，提出了带有原子函数af的kripke
af
结构，定义如下：
[0084]
定义5.3(kripke
af
)kripke
af
结构是一个四元组m
af
＝(s，s0，ap，af，r)，其中：
[0085]
(1)s是一个有限状态集合；
[0086]
(2)s0是一个有限初始状态集合；
[0087]
(3)af是原子函数的有限集合；
[0088]
(4)r是一个迁移关系，其中r是左总的，即
[0089]
(5)ap是原子命题的有限集合。
[0090]
在kripke
af
结构中，af由原子函数组成，原子函数是一个状态映射函数f，在这个函数下，每个状态都有自己的实数值。
[0091]
μ
f
语言是一个对传统的μ演算的一个扩展。从语法角度来讲，它和μ演算都拥有μ、v算子、合取∧、析取v以及[a]、<a>算子。然而，从语义角度来讲，μ
f
与μ演算的区别非常明显。μ
f
的输入与输出都是一个从状态映射到实数值的函数，而μ演算的输入是描述该性质的公式，输出值是所有满足性质的状态组成的集合，如下给出μ
f
语法和语义定义。
[0092]
定义5.4(μ
f
语法规则)af为原子函数集合，f
ap
∈af，原子函数由原子命题转换而来。令var＝{q1，q2，q3，
…
}是函数变量集合，每个q∈var可被赋值为g(s)的一个元素，g(s)是所有可能的状态函数组成的集合。μ
f
公式按如下规则构造：
[0093]
(1)如果f
ap
∈af，那么f
ap
是一个公式；
[0094]
(2)一个函数变量是一个公式；
[0095]
(3)如果f和g是公式，那么f∨g，f∧g都是公式；
[0096]
(4)如果f是公式，那么[a]f，<a>f是公式；
[0097]
(5)如果q∈var且f是一个公式，那么若f在q中是语法单调的，则μ
r
q.f，v
r
q.f是公式。
[0098]
其中，公式[a]f的直观含义是“通过a变迁的所有后继在函数f上的最小值，若没后继，则取函数最大值”；类似地，<a>f则表示“通过a变迁的所有后继在函数f上的最大值，若没后继，则取函数最小值”。
[0099]
定义5.5(μ
f
语义解释)公式f可以解释为一个状态实数映射函数f：s
→
r，可以将这个函数记为[[f]]em，其中m是变迁系统，e：var
→
g(s)是环境。新的环境记为e[q
←
w]，它与环境e的区别在于满足e[q
←
w](q)＝w。函数[[f]]em如下定义：
[0100]
(1)如果h＝[[f
{p}
]]em，那么
[0101][0102]
(2)[[q]]em＝e(q)；
[0103]
(3)如果h＝[[f∧g]]em，那么h(s)＝min{f(s)，g(s)}；
[0104]
(4)如果h＝[[f∨g]]em，那么h(s)＝max{f(s)，g(s)}；
[0105]
(5)如果h＝[[<a>f]]em，那么
[0106]
[0107]
，其中
[0108]
(6)如果h＝[[[a]f]]em，那么
[0109][0110]
，其中
[0111]
(7)[[μ
r
q.f]]em是谓词转换τ：g(s)
→
g(s)的最小不动点，其中τ的定义是τ(w)＝[[f]]e[q
←
w]m；
[0112]
(8)[[v
r
q.f]]em是谓词转换τ：g(s)
→
g(s)的最大不动点，其中τ的定义是τ(w)＝[[f]]e[q
←
w]m。
[0113]
4.μ
f
语义存在性证明
[0114]
对于μ
f
语言的语义存在性证明，实际上可以转化为证明其最小最大不动点的存在性，本发明使用tarski不动点定理对其进行证明，而在使用tarski不动点定理前，需要先证明是一个完备格。偏序集以及完备格命题证明如下：
[0115]
证明5.1(偏序集证明)是一个偏序集，其中表示对于每个集合s中的元素s， f1(s)≤f2(s)。g(s)是所有可能的状态函数组成的集合。
[0116]
证明：
[0117]
(1)自反性：对于任意的f∈g(s)，
[0118]
(2)反对称性：对于任意的f，h∈g(s)，
[0119]
(3)传递性：对于任意的f，h，r∈g(s)，
[0120]
证明5.2(最大上界存在性及完备格证明)任取g(s)中任一子集令 a(s)＝{f1(s)，f2(s)，f3(s)，
…
}的最小上界为supa(s)＝max{f1(s)，f2(s)，f3(s)，
…
}
[0121]
证明：
[0122]
(1)supa∈g(s)；
[0123]
(2) (3)则
[0124]
由此，可以得出是完备格。
[0125]
令f
min
的每个s都取最小值a，那么f
min
就是g(s)的最小元；令f
max
的每个s都取最大值b，那么f
max
就是g(s)的最大元。
[0126]
证明5.3(τ函数单调性证明)对于μ
r
的每个逻辑运算符都是单调的。
[0127]
证明：
[0128]
(1)f∧g：有
[0129]
(2)f∨g：有
[0130]
(3)[a]f：有
[0131]
(4)<a>f：有
[0132]
因此出现在不动点运算符中的公式都是单调的，进而τ函数也是单调的(即因此出现在不动点运算符中的公式都是单调的，进而τ函数也是单调的(即)。根据tarski不动点定理可以得知，μ
f
语言的最大最小不动点是存在的，即μ
f
语义是合理的。
技术特征：1.面向cps的μ演算实数值性能评价方法，其特征在于：主要包含以下步骤：(1)基于形式化方法对kripke结构引入原子函数，在kripke(s，s0，ap，r)的定义中增加一元组(af)；(2)将μ演算的语义解释从状态集合推广至{0，1}的函数；(3)对推广至{0，1}函数的mu演算进行扩展，将函数的值域从{0，1}扩展至实数值域r，并以此提出新的性能评价语言μr；(4)对μr性能评价语言中的语义解释环境进行偏序集证明、最大上界存在及完备格证明以及τ函数单调性证明。(5)完成μ演算性能评价语言扩展方法。2.根据权利1要求所描述的面向cps的μ演算实数值性能评价方法，其特征在于：所描述步骤(1)对kripke结构引入原子函数，有以下一个元组(af)：(1)af是原子函数的有限集合，每一个状态都有与之相对应的原子函数，即该状态下原子命题满足时，其函数取值为1，否则为0。3.根据权利1要求所描述的面向cps的μ演算实数值性能评价方法，其特征在于：所描述步骤(2)将μ演算的语义解释从状态集合推广至{0，1}的函数，其包含以下五个主要转换：(1)原子命题公式的语义解释转换；(2)合取逻辑算子公式的语义解释转换；(3)析取逻辑算子公式的语义解释转换；(4)<a>算子公式的语义解释转换；(5)[a]算子公式的语义解释转换。4.根据权利1要求所描述的面向cps的μ演算实数值性能评价方法，其特征在于：所描述步骤(3)将函数的值域从{0，1}扩展至实数值域r，并以此提出新的性能评价语言μr：首先根据步骤(2)的转换将集合转换为函数，再将函数的值域从{0，1}扩展至整个实数域r。再根据这个函数提出相应的μr性能评价语言的语法和语义。5.根据权利1要求所描述的面向cps的μ演算实数值性能评价方法，其特征在于：所描述步骤(4)对μr性能评价语言中的语义解释环境进行偏序集证明、最大上界存在及完备格证明以及τ函数单调性证明：根据μr性能评价语言中的语义环境，对τ函数的值域以及其计算方法进行相应的偏序集证明、完备格证明，再对整个τ函数进行单调性证明，最后通过tarski不动点定理证明μr语言中提出的不动点的存在性，即μr语言的合理性。
技术总结本发明公开了面向CPS的μ演算实数值性能评价方法。本发明使用Kripke结构作为基本的迁移系统进行解释，并在此基础上提出带有原子函数的Kripke结构。本发明通过从集合推广至函数的方法将μ演算的输出值从布尔域推广至实数域，从而实现性能评价方法。本发明在推广至函数值的μ演算的基础上提出了新的性能评价语言
技术研发人员：朱一峰 曹子宁 王福俊
受保护的技术使用者：南京航空航天大学
技术研发日：2021.03.01
技术公布日：2021/6/29
