基于不动点逻辑的混成系统性能评价语言
时间：2023-06-18 08:00:04 来源：雅意学习网 本文已影响 人 
李 晴，曹子宁,2,3，黄 涛
(1.南京航空航天大学 计算机科学与技术学院，江苏 南京 211106;2.光电控制技术重点实验室，河南 洛阳 471023;3.软件新技术与产业化协同创新中心，江苏 南京 210023)
混成系统[1](Hybrid System，HS)通常由离散组件和连续组件组成，二者互相影响、互相依赖[2]。并且随着混成系统的设计越来越复杂，二者之间的交互越来越紧密。目前，它已广泛应用在智能电网、自动公路系统和医疗机器人等各种安全关键领域[3]。它们对系统的安全性有极高的要求，然而通过模型检测等常用的形式化方法保障其安全性是很有限的。因此，需要将模型检测与性能评价相结合[4]，利用各自的优点，在保证验证系统效率的同时，描述更多系统的属性。
文献[5]提出PLTL用于描述“系统最终不会到达死锁状态的概率是否小于等于0.9？”等系统性质。文献[6]提出了计算树度量语言CTML，用于评价系统与实数计算相关的性质，如概率、平均期望等。文献[7]在CTML、ZIA的基础上，提出了PZIA，用于描述系统与数据相关的性质和行为的概率性质等。
基于μ演算[8-9]的模型检测可用于设计与验证并发系统[10]，通过使用不动点算子刻画系统的性质。文献[11-12]在不动点算子的基础上分别提出并发加权μ演算和广义可能性μ演算以增强经典μ演算的表达能力。此外，目前已有一些较为高效的算法用于评价μ演算的公式[10,13]，并且很多时序逻辑可以转换为μ演算，比如CTL。
因此，结合CTML和μ演算，该文提出了基于不动点的性能评价语言MLBoF。由于MLBoF公式包含不动点，而不动点的存在不是必然的，因此给出其语义存在的合理性证明。为了简化CTML子逻辑的计算步骤，给出与其语义等价的MLBoF公式及相应的证明过程。最后，给出MLBoF公式的性能评价算法。
为了提出能够描述实值计算相关性质的性能评价语言，通过对经典Kripke结构中的标签函数进行扩展，将标签函数L的值域从{0,1}扩展为[m,n]，其中m 定义1(状态标签函数)：状态标签函数f表示从状态空间S到闭区间[m,n]的一个映射，它可以表示为：f:S→[m,n]。其中，m和n的取值取决于具体实例。 状态标签函数也可称为原子函数或状态函数，带有原子函数的Kripke结构定义如下： 定义2(KripkeAF)：KripkeAF结构是一个四元组MAF=(S,S0,AF,R)，其中，S是一个有限状态集合； KripkeAF为提出可以描述系统实值计算相关性质的新的性能评价语言奠定了基础。 MLBoF作为CTML和μ演算部分结合的产物，其语法定义如下所述： 定义3(MLBoF语法)：AF为原子函数集合，令fp表示由原子命题转换而来的状态函数，AF由一般的状态函数f和fp组成。令VAR={φ1,φ2,φ3,…}，表示函数变量集合，其中每个φ∈VAR可被赋值为G(S)的一个元素，G(S)是所有可能的状态函数组成的集合。MLBoF公式按如下规则构造： (1)若fAF∈AF，则fAF是一个公式； (2)一个函数变量φ是一个公式； (3)若f和g是公式，则f·g,f∨g,f∧g也是公式； (4)如果f是公式，那么MXf是公式； (5)若φ∈VAR是一个公式且f是一个公式，又f在φ上是单调的(由于MLBoF公式的构造中去除了否定算子，即f中出现的所有函数变量φ，在公式f中其外面嵌套的否定算子个数为0)，则μφ·f和νφ·f都是公式。 经典的μ演算公式表示一个状态集合，而MLBoF的公式表示一个函数。MLBoF的语义定义如下所示： 定义4(MLBoF语义)：公式f可以解释为一个状态映射函数f:S→[m,n]，并将其记为[[f]]Me，其中M是变迁系统，e:VAR→G(S)是环境。函数[[f]]Me的递归定义如下所示： (1)若h=[[fAF]]Me，则存在两种情况：若fAF=f，则对于∀s∈S，存在h(s)=f(s)； (2)[[φ]]Me=e(φ)。 (3)若h=[[f·g]]Me，则对∀s∈S，有h(s)=f(s)·g(s)； (4)若h=[[MXf]]Me，则对∀s∈S，有： 其中，Ts={t|s→t,且s≠t}，ps,t是由状态s到状态t的迁移概率。 (5)若h=[[f∧g]]Me，则对∀s∈S，有h(s)=min{f(s),g(s)}。 (6)若h=[[f∨g]]Me，则对∀s∈S，有h(s)=max{f(s),g(s)}。 (7)若h=[[μφ.f]]Me，则[[μφ.f]]Me是变换τ:G(S)→G(S)的最小不动点，其中τ(W)=[[f]]Me[φ←W]。 (8)若h=[[νφ.f]]Me，则[[νφ.f]]Me是变换τ:G(S)→G(S)的最大不动点，其中τ(W)=[[f]]Me[φ←W]。 由于性能评价语言MLBoF的语义涉及到不动点，而不动点是否存在并不是显然的。因此，MLBoF语义的合理性依赖于不动点的存在，进而下文对不动点的存在性进行论述。 根据Tarski不动点定理，若MLBoF公式的语义解释环境构成完备格以及映射函数τ是单调的，那么可证得不动点是存在的。 下面给出基于MLBoF公式语义的G(S)上的二元关系定义，以及该二元关系是偏序关系的证明过程，具体如下： 定义5(二元关系≼)：给定一个KripkeAF结构M=(S,S0,AF,R)，S上所有的状态函数构成集合G(S)，G(S)上存在一个二元关系≼：对于函数f1,f2∈G(S)，若对∀s∈S，f1(s)≤f2(s)成立，则称f1≼f2成立。 命题1：G(S)上的二元关系集合(G(S),≼)是偏序集。 证明：根据≼和偏序的定义，可证得≼满足自反性、反对称性和传递性。因此，命题1成立，具体的证明过程见文献[14]。 命题2：偏序集(G(S),≼)构成一个完备格。 证明：根据完备格[11]和(G(S),≼)的定义，取G(S)中任一子集A(S)。考虑A(S)的最小上界分别是A(S)和G(S)A(S)中的元素两种情况，可证得G(S)的任意子集A(S)存在最小上界和最大下界。具体的证明过程见文献[14]。 在此基础上，可以利用结构归纳法证明G(S)上的映射函数τ:G(S)→G(S)的单调性。而τ函数的单调性证明可转化为MLBoF公式的单调性证明，进而可转化为MLBoF公式中出现的所有算子的单调性证明。 命题3：MLBoF公式中出现的所有算子都是单调的。 证明：根据基础算子·、MX、∧和∨的语义及利用其构造的MLBoF公式语义，可证得基础算子·、MX、∧和∨的是单调的。因此，命题3成立，具体的证明过程见文献[14]。 因此，由上述算子构造的MLBoF的任何公式也是单调的。由于不动点算子中的公式是·、∧、∨和MX算子构成的，所以出现在不动点算子中的每一个可能的公式也是单调的。根据结构归纳法，不动点算子构成的MLBoF公式也是单调的。而G(S)上的映射函数τ是由·、∧、∨和MX和不动点算子构成的，因此，根据结构归纳法，若构成τ函数的基础算子是单调的，那么τ函数也是单调的。 由Tarski不动点定理，可知MLBoF存在最小和最大不动点。所以其语义是合理的。 利用结构归纳法的思想，可将μ演算中谓词变换满足∪连续和∩连续定义和性质[15]推广到MLBoF上的映射函数τ(W)=[[f]]Me[φ←W]，因此τ(W)=[[f]]Me[φ←W]也是∪连续和∩连续的。而根据MLBoF的语法和语义可知，μφ.f和νφ.f的语义(即[[μφ.f]]Me和[[νφ.f]]Me分别表示映射函数τ(W)=[[f]]Me[φ←W]的最小不动点和最大不动点。 因此，根据Tarski不动点定理可知，若τ是∪连续的，则[[μφ.f]]Me=∪i(τi(MIN))； CTML是一个可用于描述系统的概率和期望等实值属性的性能评价语言，它的某些子逻辑可以用MLBoF表示，该文将它们命名为SLoCTML(Sub-Logic of CTML)。它的语法和语义具体如下： 定义6(SLoCTML语法)：SLoCTML的语法定义如下： (1)φ::=one|zero|r|φ·φ|Mδ； (2)δ::=φU×φ|Xφ； 由于SLoCTML代表CTML的某些子逻辑，其更加具体的语法解释和语义定义可见文献[6]。 根据二者的语义，可知MLBoF公式可以表示SLoCTML，如MX、·、MU×，而且SLoCTML的原子状态函数可以用MLBoF的原子状态函数fp表示。 根据SLoCTML的语义可知，SLoCTML的MU×算子描述的系统属性相对复杂，具有较大的实际意义。所以下文以MU×为例，给出与其语义等价的MLBoF公式表示以及证明过程。 由于性能评价语言MLBoF的公式涉及到不动点，表达形式比较抽象，不利于理解和描述性质。根据二者公式语义，可知M(fU×g)与μφ.[g∨(f·MXφ)]语义等价，且τ(φ)=g∨(f· MXφ)。若状态s满足M(fU×g)，则使用上述语义等价的MLBoF公式计算； 在证明语义等价前，需要进行一些说明： (1) 将SLoCTML的MU×公式中出现的原子命题f和g看作MLBoF中的原子函数，并且它们的值域为实数区间[m,n]中，其中m=0，n=1。 (2)令最大的状态函数和最小的状态函数分别为MAX:S→{n}和MIN:S→{m}。 下面给出二者语义等价的具体证明过程： 命题4：τ(φ)=g∨(f· MXφ)是单调的。 证明：假设f1≼f2，根据函数τ(φ)=g∨ (f· MXφ)的语义，给出τ(f1)和τ(f2)各自可能的两种语义。并在此基础上，根据偏序关系≼的定义、τ(f1)和τ(f2)每种可能语义之间的依赖关系，进而证得τ(f1)≼τ(f2)成立。具体的证明过程见文献[14]。 命题5：M(fU×g)的语义和τ(φ)=g∨(f·MXφ)的不动点的语义等价。 证明：综合考虑M(fU×g)可能的两种语义h(s)=g(s)和h(s)=(f· MX (MfU×g))(s)，利用公式转换和具体的公式语义可证得命题5成立，具体的证明过程见文献[14]。 命题6：CTML的M(fU×g)公式的语义和MLBoF的μφ.[g∨ (f·MXφ)]公式语义等价，即M (fU×g)=[[μφ.[g∨ (f·MXφ)]]]Me。 证明：在分析公式μφ.[g∨ (f· MXφ)]和M(fU×g)的语义之后，利用归纳法，依次证得∪i(τi(MIN))≼M(fU×g)和M(fU×g)≼∪i(τi(MIN))成立。因此，命题6成立。具体的证明过程见文献[14]。 该算法是对Emerson和Lei提出的用于评价μ演算公式的算法[15]的一个扩展，其不同之处在于在计算外层不动点的新的近似值时，不必使用MIN或MAX重新初始化内层不动点的计算，只需从这个不动点下的任何已知的近似值开始迭代计算即可。此外，通过引入人为设置的误差值α，避免算法进行无终止地计算。所以，该算法能够在保证效率的同时，尽可能地计算出较为接近真正不动点的近似不动点。 MLBoF公式的性能评价算法输入MLBoF公式、系统模型KripkeAF和误差值α，输出一个状态函数h。该算法的伪代码如下所示： 1:Function eval (h,e) 2:if (h=fp) 3: forsinS 4:if (p∈L(s))h(s)=1; 5:Elseh(s)=0; 6: returnh; 7:if (h=f) 8: forsinSh(s)=f(s); 9: returnh; 10:if (h=φ) returne(φ); 11:if (h=g1·g2) 12:g1=eval(g1,e);g2= eval(g2,e); 13: forsinSh(s)=g1(s)·g2(s); 14: returnh; 15:if(h=g1∧g2) 16:g1=eval(g1,e);g2= eval(g2,e); 17: forsinSh(s)=min{g1(s),g2(s)}; 18: returnh; 19:if (h=g1∨g2) 20:g1= eval(g1,e);g2=eval(g2,e); 21: forsinSh(s)=max{g1(s),g2(s)}; 22: returnh; 23:if(h= MXg) 24:g=eval(g,e); 25: forsinS 27: Elseh(s)=g(s); 28: returnh; 29:if (h=μφi.f(φi)) 30: for top-level greatest fixpoint subformulasυφj.f"(φj) inf 31:F[j]=MAX; 32: while ∀s∈S,F[j](s)-φold(s)>α 33:φold=F[i]; 34:F[i]= eval(f,e[φi←F[i]]); 35:h=F[i]； 36: returnh; 37:if (h=νφi.f(φi)) 38: for top-level least fixpoint subformulasμφj.f"(φj) inf 39:F[j]=MIN; 40: while ∀s∈S,F[i](s)-φold(s)>α 41:φold=F[i]; 42:F[i]=eval(g,e[φi←F[i]]); 43:h=F[i]； 44: returnh; 45:end function eval; 本节以飞机起飞控制系统[16]为例，使用MLBoF和CTML公式分别描述与其本身相关的系统性质，并使用MLBoF公式的性能评价算法计算MLBoF公式的值。 它的整个起飞过程由停止、滑行、起飞、爬升、平飞等阶段组成，并且前四个阶段有可能进入故障状态。它的自动机模型如图1所示。 图1 飞机控制系统 (1)对于性质“飞机从Stop开始，最终发生异常即到达Error状态的概率是多少”， CTML描述为：(Mone U×fError) (Stop)， MLBoF公式描述为：μφ.[fError∨ (one · MXφ)]，τ(φ)=fError∨ (one · MXφ)。需要注意的是，下面公式中的S的元素依次为状态Stop、Taxi、Take_off、Climb、Error和Cruise。 其中，MLBoF公式分别由CTML中的原子命题one和fError转换而来。因此，其映射的实数区间为[0,1]，并且MIN:S→{0}。根据性能评价算法，令误差α=0.001，有： τ(MIN)(S)=(0,0,0,0,1,0)； τ2(MIN)(S)=(0.1, 0.1, 0.1, 0.1, 1, 0)； τ3(MIN)(S)=(0.19, 0.19, 0.19, 0.1, 1, 0)； τ4(MIN)(S)=(0.271, 0.271, 0.19,0.1,1,0)； τ5(MIN)(S)=(0.343 9,0.271,0.19,0.1,1,0)； τ6(MIN)(S)=τ5(MIN) (S)。 此时算法终止，可知飞机从Stop开始，最终发生异常即到达Error状态的概率是0.343 9。 (2)对于性质“飞机从Stop开始，最终成功巡航即到达Cruise状态的概率是多少”，CTML描述为：(M oneU×fCruise)(Stop)， MLBoF公式描述为：μφ.[fCruise∨ (one · MXφ)]，τ(φ) =fCruise∨ (one · MXφ)。 根据性能评价算法，令误差α=0.001，有： τ(MIN)(S) = (0, 0, 0, 0, 0, 1)； τ2(MIN)(S) = (0, 0, 0, 0.9, 0,1)； τ3(MIN)(S) = (0, 0, 0.81, 0.9, 0, 1)； τ4(MIN)(S) = (0, 0.729, 0.81, 0.9, 0, 1)； τ5(MIN)(S)=(0.656 1, 0.729,0.81, 0.9,0,1)； τ6(MIN)(S) =τ5(MIN)(S)； 此时算法终止，可知飞机从Stop开始，最终成功巡航即到达Cruise状态的概率是0.656 1。 通过上述应用实例可知，MLBoF公式的性能评价算法的效率体现在以下两个层面： (1)由于MU×公式的计算依赖于涉及矩阵方程等复杂计算的线性系统求解[6]，计算复杂，且时间复杂度为O(Poly(|S|)。其中Poly(|S|)表示|S|大小的多项式时间，|S|表示系统模型中的状态个数。而与MU×公式语义等价的MLBoF公式的计算依赖于计算不动点的思想，该过程无需进行复杂的数学计算。因此，从这个层面上讲，该算法的效率体现在算法思想和计算步骤的简单。 (2)由于MLBoF公式的性能评价算法的提出基于对需要进行O(nd)次迭代的计算不动点的算法的扩展，相对于扩展需要进行O(nk)次迭代的简单直接的递归算法，该算法的效率更高。其中，n表示系统模型的状态个数，k表示不动点嵌套深度，d表示公式的交替深度[15]。因此，从这个层面上，该算法的效率也得到了一定的改善。 由于混成系统广泛应用于各种安全关键领域，通过一般的形式化方法保障其安全性有一定的局限性。因此，提出一种面向混成系统的性能评价语言MLBoF，用于描述系统行为的概率属性等。同时，为了简化SLoCTML的计算步骤以及提高MLBoF公式的理解性，给出与SLoCTML语义等价的MLBoF公式。最后，通过扩展计算不动点的算法，提出一个MLBoF公式的性能评价算法。与传统的基于μ演算的模型检测[15]相比，MLBoF可以描述系统行为的概率属性。在以后的工作中，可以尝试往MLBoF公式中引入更多的算子如+算子，使其能够描述完整的CTML逻辑。
S0是一个有限初始状态集合；
AF是原子函数的有限集合；
R是一个迁移关系，R⊆S×S，R满足∀s∈S,∃s"∈S，使(s,s")∈R。1.1 MLBoF语法
1.2 MLBoF语义
若fAF=fp，则对于∀s∈S，存在：
需要注意，使用·算子的前提是公式f和g满足f:S→[0,1]和g:S→[0,1]，并且[0,1]⊆[m,n]。
若τ是∩连续的，则[[νφ.f]]Me=∩i(τi(MAX))。假设G(S)中的所有函数映射的值都位于实数区间[m,n],那么MIN表示fmin:S→{m}，MAX表示fmax:S→{n}。3.1 CTML简介
3.2 与MU×公式语义等价的MLBoF公式
否则，对于不满足路径公式的状态s，令其函数值为0。
