技术领域
本发明公开了一种面向CPS的μ演算实数值性能评价方法，主要用于对CPS使用形式化验证的方法进行系统验证，并通过输出为实数值的性能评价语言进行系统度量分析。
背景技术
信息物理融合系统(CPS)是基于行为离散、时间连续的复杂混成系统，同时在实际应用中，还可能夹杂着不确定性、资源消耗性等各种附带信息的属性。这种混成系统在现实生活中受到了广泛的运用，而在受到人们广泛运用的同时，混成系统的安全性和可靠性也变得尤为重要。因此，保证这类混成系统的安全性和可靠性也成为了目前的主要研究方向。模型检测技术是一个基于有限状态的形式化验证技术，通过对系统进行形式化的建模，并采用可以描述形式化模型的相应逻辑语言来表达需要验证的性质，并将性质由公式的形式所表达出来，通过模型检测算法进行相应的验证。目前模型检测技术通常使用的经典模型有有限状态自动机、时间自动机、概率自动机、混成自动机以及进程代数CSP(Communication Sequential Process)、CCS(Calculus of Communicating Systems)等，经典时序逻辑有线性时序逻辑 LTL(Linear Temporal Logic)和计算树逻辑CTL(Computation Tree Logic)。
针对CPS的不确定性和时间消耗性，经典的LTL和CTL时序逻辑语言没有足够的能力刻画相应的性质，因此有学者在前两者的基础上添加了概率算子和时间算子，提出了概率计算树逻辑PCTL(Probabilistic Computation Tree Logic)、概率线性时序逻辑PLTL(Linear Temporal Logic with Probability)以及时间计算树逻辑TCTL(TimedComputation Tree Logic)，并分别给出了模型检测算法。然而即使增加了时间或概率算子，能够刻画出相应的概率性质和时间性质，但仍然无法对具体的实数值进行刻画。换言之，传统的模型检测技术仅仅是对所要验证的一个性质公式进行形式化验证，而后得出相应的布尔值，即True或False，而并不能得到满足某个性质的条件下，会花费多少时间，或者以多大/小的概率能够满足该性质。为了解决这类传统的时序逻辑语言遇到的问题，本发明通过已有的性能评价语言CTML (Computation Tree Measurement Language)以及传统的μ演算提出了一个表达能力较强的的性能评价语言——μR。
发明内容
信息物理融合系统存在着不确定性且伴随资源消耗。由于传统的μ演算无法描述需要输出实数值的性质，而其表达能力却非常强大，因此本发明在其基础上，与性能评价方法相结合，将μ演算通过函数的方法转换至性能评价方法中。
本发明是一种面向CPS的μ演算实数值性能评价方法，主要包括以下步骤：
步骤1：对Kripke结构引入原子函数，有以下一个元组(AF)
AF是原子函数的有限集合，每一个状态都有与之相对应的原子函数，即该状态下原子命题满足时，其函数取值为1，否则为0。
步骤2：将μ演算的语义解释从状态集合推广至{0，1}的函数，其包含以下五个主要转换
(1)原子命题公式的语义解释转换；
(2)合取逻辑算子公式的语义解释转换；
(3)析取逻辑算子公式的语义解释转换；
(4)算子公式的语义解释转换；
(5)[a]算子公式的语义解释转换。
步骤3：将函数的值域从{0，1}扩展至实数值域R，并以此提出新的性能评价语言μR
首先根据步骤2的转换将集合转换为函数，再将函数的值域从{0，1}扩展至整个实数域R。再根据这个函数提出相应的μR性能评价语言的语法和语义。
步骤4：对μR性能评价语言中的语义解释环境进行偏序集证明、最大上界存在及完备格证明以及τ函数单调性证明
根据μR性能评价语言中的语义环境，对τ函数的值域以及其计算方法进行相应的偏序集证明、完备格证明，再对整个τ函数进行单调性证明，最后通过Tarski不动点定理证明μR 语言中提出的不动点的存在性，即μR语言的合理性。
本发明根据信息物理融合系统的实际特性以及现有的性能评价语言对μ演算进行了扩展，使其能够足以描述信息物理融合系统的不确定性、资源消耗等性质的度量分析，同时使用 Tarski不动点定理证明扩展后的语言的正确性，为后续进一步的形式化验证和分析工作奠定基础。
附图说明
图1为面向CPS的μ演算实数值性能评价方法的流程图
图2为Kripke结构例子
具体实施方式
本发明的实施提供了一种面向CPS的μ演算实数值性能评价方法，为使本领域技术人员更好地理解本发明的技术方案，下面结合附图和具体实施方式对本发明作进一步详细描述。通过参考附图描述的实施方式是示例性的，仅用于解释本发明，而不能解释为对本发明的限制。
本发明的目的是，为了解决表达能力非常强大的μ演算无法对复杂的信息物理融合系统进行直接的性能评价的目的，针对其语义解释的集合性质，通过函数的方法将其输出值从布尔域扩展至实数域，并由此提出新的性能评价语言μR用来对CPS的概率、权值等属性进行性能评估。
面向CPS的μ演算实数值性能评价方法的流程如附图1所示。具体的发明实施方法如下：
1.从布尔域到实数域的扩展
对于传统的模型检测技术和算法而言，性能评价语言与之最大的区别就是输入与输出的值域的不同。在传统的形式化验证方法中，
通常使用布尔值(True或False)作为输出，来判断输入的公式是否为该系统满足的属性；而在性能评价语言中，则将输出从布尔值推广到实数值，可以对整个系统在某个状态下满足某个公式所需要的度量值进行量化的计算，得出一个具体或近似的实数值来。本发明将把μ演算的输出值推广至实数域，使用Kripke结构作为基本的迁移系统进行解释，并给出推广为实数域的语言μ
在给出μ
定义5.1(Kripke)Kripke结构是一个五元组M＝(S，S
(1)S是一个有限状态集合；
(2)S
(3)AP是原子命题的有限集合；
(4)R是一个迁移关系，
(5)L是一个标签函数，S→2
如图2所示，M＝(S，S
(1)状态集S是{s
(2)初始状态集为{s
(3)原子命题集合是{p，q}；
(4)迁移关系有{(s
(5)L(s
2.μ演算从集合推广至函数
本发明主要的研究内容是将形式化验证语言从布尔值推广至实数值，而对于μ演算而言，其语义是将系统中满足该公式的所有状态作为集合来输出，与经典的时序逻辑有所不同。因此，本发明先将其输出从集合推广为函数。
传统的μ演算公式是一个满足性质的状态集合，我们可以把这个集合看作是一个从状态集合到{0，1}的函数F：S→{0，1}，其中每个状态都映射到0或1，当这个状态满足该性质时，该状态将映射到1，反之则映射为0。以上面的Kripke结构M为例，对于每一种公式，如下给出相应的变换：
(1)原子命题公式的语义解释转换[[p]]
公式p与公式q是原子命题，由Kripke结构M可以得出：
[[p]]eM＝{s|p∈L(s)}＝{s
[[q]]eM＝{s|q∈L(s)}＝{s
将集合{s
将集合{s
那么公式p的语义解释从集合变为函数F
(2)合取逻辑算子公式的语义解释转换[[h]]eM＝[[f∧g]]eM：
将原子命题公式p作为公式f，q作为公式g，那么根据(1)可知：
[[f]]eM＝[[p]]eM＝{s
[[g]]eM＝[[q]]eM＝{s
[[h]]eM＝[[f∧g]]eM＝[[f]]eM∩[[g]]eM＝{s
将集合{s
那么公式h的语义解释从集合变为函数F
而从函数的计算来看，则是对F
(3)析取逻辑算子公式的语义解释转换[[h]]eM＝[[f∨g]]eM：
将原子命题公式p作为公式f，q作为公式g，那么根据(1)可知：
[[f]]eM＝[[p]]eM＝{s
[[g]]eM＝[[q]]eM＝{s
[[h]]eM＝[[f∨g]]eM＝[[f]]eM∪[[g]]eM＝{s
将集合{s
那么公式h的语义解释从集合变为函数F
而从函数的计算来看，则是对F
(4)算子公式的语义解释转换[[k]]eM＝[[h]]eM：
将原子命题公式p作为公式f，q作为公式g，h为f∧g，那么根据(1)(2)可知：
将集合{s
那么公式k的语义解释从集合变为函数F
而从函数的计算来看，则是对F
(5)[a]算子公式的语义解释转换[[k]]eM＝[[[a]h]]eM：
将原子命题公式p作为公式f，q作为公式g，h为f∧g，那么根据(1)(2)可知：
将集合{s
那么公式k的语义解释从集合变为函数F
而从函数的计算来看，则是对F
由上述每一个算子从状态集合到状态函数的转换，将函数的值域从{0，1}扩展至[a，b]，其中a，b为非零实数，a＜b，那么就可以对相关性质度量进行实数计算。
3.μ
μ
定义5.2(状态映射函数f)μ
f：S→[a，b]
在经典的Kripke结构中，每个状态内都有一个或多个原子命题，这些原子命题通过标签函数L进行描述。而针对μ
定义5.3(Kripke
(1)S是一个有限状态集合；
(2)S
(3)AF是原子函数的有限集合；
(4)R是一个迁移关系，
(5)AP是原子命题的有限集合。
在Kripke
μ
定义5.4(μ
(1)如果f
(2)一个函数变量是一个公式；
(3)如果f和g是公式，那么f∨g，f∧g都是公式；
(4)如果f是公式，那么[a]f，f是公式；
(5)如果Q∈VAR且f是一个公式，那么若f在Q中是语法单调的，则μ
其中，公式[a]f的直观含义是“通过a变迁的所有后继在函数f上的最小值，若没后继，则取函数最大值”；类似地，f则表示“通过a变迁的所有后继在函数f上的最大值，若没后继，则取函数最小值”。
定义5.5(μ
(1)如果h＝[[f
(2)[[Q]]eM＝e(Q)；
(3)如果h＝[[f∧g]]eM，那么h(s)＝min{f(s)，g(s)}；
(4)如果h＝[[f∨g]]eM，那么h(s)＝max{f(s)，g(s)}；
(5)如果h＝[[f]]eM，那么
，其中
(6)如果h＝[[[a]f]]eM，那么
，其中
(7)[[μ
(8)[[v
4.μ
对于μ
证明5.1(偏序集证明)
证明：
(1)自反性：对于任意的f∈G(S)，
(2)反对称性：对于任意的f，h∈G(S)，
(3)传递性：对于任意的f，h，r∈G(S)，
证明5.2(最大上界存在性及完备格证明)任取G(S)中任一子集
证明：
(1)supA∈G(S)；
(2)
由此，可以得出
令f
证明5.3(τ函数单调性证明)对于μ
证明：
(1)f∧g：
(2)f∨g：
(3)[a]f：
(4)f：
因此出现在不动点运算符中的公式都是单调的，进而τ函数也是单调的(即
机译： 抗菌材料性能的确认方法，抗菌材料性能的确认方法，抗菌材料活性的评价方法，抗菌材料的性能评价方法，抗菌材料的性能评价方法，对材料的效度评价方法材料表面
机译： 面向真实世界的用户界面设备和面向真实世界的用户界面程序
机译： 面向数值信息的性能分析系统
