[發(fā)明專利]面向CPS的μ演算實數(shù)值性能評價方法

在審

• 申請?zhí)枺?/td>: 202110227457.6
• 申請日: 2021-03-01
• 公開（公告）號: CN113051714A
• 公開（公告）日: 2021-06-29
• 發(fā)明（設(shè)計）人: 朱一峰;曹子寧;王福俊
• 申請（專利權(quán)）人: 南京航空航天大學(xué)
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F111/08
• 代理公司: 暫無信息
• 代理人: 暫無信息

1.面向CPS的μ演算實數(shù)值性能評價方法，其特征在于：主要包含以下步驟：

(1)基于形式化方法對Kripke結(jié)構(gòu)引入原子函數(shù)，在Kripke(S，S0，AP，R)的定義中增加一元組(AF)；

(2)將μ演算的語義解釋從狀態(tài)集合推廣至{0，1}的函數(shù)；

(3)對推廣至{0，1}函數(shù)的mu演算進行擴展，將函數(shù)的值域從{0，1}擴展至實數(shù)值域R，并以此提出新的性能評價語言μR；

(4)對μR性能評價語言中的語義解釋環(huán)境進行偏序集證明、最大上界存在及完備格證明以及τ函數(shù)單調(diào)性證明。

(5)完成μ演算性能評價語言擴展方法。

2.根據(jù)權(quán)利1要求所描述的面向CPS的μ演算實數(shù)值性能評價方法，其特征在于：所描述步驟(1)對Kripke結(jié)構(gòu)引入原子函數(shù)，有以下一個元組(AF)：

(1)AF是原子函數(shù)的有限集合，每一個狀態(tài)都有與之相對應(yīng)的原子函數(shù)，即該狀態(tài)下原子命題滿足時，其函數(shù)取值為1，否則為0。

3.根據(jù)權(quán)利1要求所描述的面向CPS的μ演算實數(shù)值性能評價方法，其特征在于：所描述步驟(2)將μ演算的語義解釋從狀態(tài)集合推廣至{0，1}的函數(shù)，其包含以下五個主要轉(zhuǎn)換：

(1)原子命題公式的語義解釋轉(zhuǎn)換；

(2)合取邏輯算子公式的語義解釋轉(zhuǎn)換；

(3)析取邏輯算子公式的語義解釋轉(zhuǎn)換；

(4)a算子公式的語義解釋轉(zhuǎn)換；

(5)[a]算子公式的語義解釋轉(zhuǎn)換。

4.根據(jù)權(quán)利1要求所描述的面向CPS的μ演算實數(shù)值性能評價方法，其特征在于：所描述步驟(3)將函數(shù)的值域從{0，1}擴展至實數(shù)值域R，并以此提出新的性能評價語言μR：首先根據(jù)步驟(2)的轉(zhuǎn)換將集合轉(zhuǎn)換為函數(shù)，再將函數(shù)的值域從{0，1}擴展至整個實數(shù)域R。再根據(jù)這個函數(shù)提出相應(yīng)的μR性能評價語言的語法和語義。

5.根據(jù)權(quán)利1要求所描述的面向CPS的μ演算實數(shù)值性能評價方法，其特征在于：所描述步驟(4)對μR性能評價語言中的語義解釋環(huán)境進行偏序集證明、最大上界存在及完備格證明以及τ函數(shù)單調(diào)性證明：根據(jù)μR性能評價語言中的語義環(huán)境，對τ函數(shù)的值域以及其計算方法進行相應(yīng)的偏序集證明、完備格證明，再對整個τ函數(shù)進行單調(diào)性證明，最后通過Tarski不動點定理證明μR語言中提出的不動點的存在性，即μR語言的合理性。