没有合适的资源?快使用搜索试试~ 我知道了~
可在www.sciencedirect.com在线获取理论计算机科学电子笔记319(2015)289-313www.elsevier.com/locate/entcs无交替加权Mu演算的可判定性和完备性Kim G.Larsen Radu Mardare Bingtian Xue薛炳天1,2丹麦奥尔堡大学摘要在本文中,我们介绍WMC,加权版本的替代自由模态μ演算加权过渡系统。WMC包含以前研究的加权扩展CTL和类似于以前提出的时间扩展版本的模态μ演算。 此外,我们还为WMC开发了一个符号语义,并证明了满足性的概念与符号满足性的概念是一致的。这个中心结果使我们能够证明WMC的两个主要的元属性。第一个是WMC的满意度的可判定性。与经典的模态μ演算不同,WMC不具有有限模型性质。尽管如此,有限模型属性仍然适用于符号语义和可判定性;这与满足性已被证明是不可判定的定时转移系统的类似逻辑形成对比。作为第二个主要贡献,我们提供了一个完整的公理化,这适用于这两种语义。完备性证明是非标准的,因为逻辑是非紧的,并且它涉及符号模型的概念。关键词:加权模态μ演算,非紧模态逻辑,加权转移系统,可满足性,完全公理化。1介绍二十多年来,人们一直在寻求规范和建模形式,以解决嵌入式和网络物理系统的基本非功能属性特别地,时间自动机[4]用于表达和分析系统关于时间逻辑的时间约束,例如TCTL [3],Tμ [17],Lν [23]和MTL [19]。然而,嵌入式系统或网络物理系统同样重要的非功能特性与资源消耗,特别是能源消耗有关。这导致最初的加权扩展的时间自动机[5,6]和最近的能量自动机[9]。然而,1本研究得到了中丹基础研究中心IDEA4CPS的部分资助2电子邮件:kgl,mardare,bingt@cs.aau.dkhttp://dx.doi.org/10.1016/j.entcs.2015.12.0181571-0661/© 2015作者。出版社:Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章(http://creativecommons.org/licenses/by-nc-nd/4.0/)。290K.G. Larsen等人/理论计算机科学电子笔记319(2015)289成本最优可达性和无限次运行的问题已被证明是有效可计算的,关于TCTL的加权扩展的一般模型检验问题被证明是不可判定的[11]。在本文中,我们考虑了纯加权设置,其中系统的定量信息被建模为加权迁移系统(WTS)的过渡被装饰的非负实数除了行动。本文研究了加权逻辑在最一般情况下的可满足性和公理化问题。我们开发了WMC,一个无选择模态μ演算的加权版本,它包含了WCTL,类似于先前研究的模态μ演算Tμ和Lν的时间扩展。WMC是一种具有固定点运算符的多模态逻辑,其中模态约束离散转换或给定状态下的资源量。对于后者,WMC使用资源变量,类似于定时逻辑中使用的时钟变量,参见例如。[10 ]第10段。我们的第一个主要贡献是展示WMC的可确定性。在以前的工作[27]中,我们证明了WMC的限制的可判定性和有限模型性质,每个资源只有一个资源变量,并且只有最大不动点。这种限制严重限制了逻辑的表达能力。在[25,26]中,我们研究了WMC的两个子逻辑,每个资源具有多个资源变量,并且只有最大不动点。这些逻辑通过使用过滤构造被证明是可判定的,但比WMC弱得多,因为资源变量被限制为事件记录。与这些片段和模态μ演算相反,WMC并不限定模型属性,因此经典论证并不具有可判定性。作为替代,我们在这里提出符号模型和语义的概念,其中有限模型属性确实成立。幸运的是--这应该与满足性不可判定的类似时间逻辑形成对比。两种语义具有相同的有效性这一事实是一个显著的性质,也是一个强大的工具,它允许我们在两种语义之间传输元结果,特别是满足性检查的可计算性和复杂性结果以及证明系统的完整性结果我们的第二个主要贡献是一个完整的公理化的WMC,允许所有有效的属性推导定理。据我们所知,这是文献中第一个完整的不动点加权模态逻辑公理化公理化非常简单,将非递归加权逻辑的模态公理与经典的不动点公理结合在一起[20,28,30]。有限模型属性提供了证明公理化对于符号语义是完备的参数,因此,完备性结果可以外推到WTS语义。我们的第三个主要贡献是完备性证明本身,它在许多方面都是非标准的和新颖由于逻辑是非紧的,它需要无限的K.G. Larsen等人/理论计算机科学电子笔记319(2015)289291−→a证据规则为了解决这个问题,我们涉及模型理论的拓扑技术,受到Rasiowa和Sikorski工作的启发[16,29]。这些技术是由前两位作者与Kozen和Panangelo合作开发的,用于证明马尔可夫逻辑的强完备性[21,22]。我们的完备性证明避免了[32]中用于一般Mu演算的tableaux方法,并且在类似的上下文中重用它是足够鲁棒的。另一方面,我们的证明是为无交替演算设计的,不清楚它是否可以在一般的无限制上下文中使用。2无交替加权μ演算定义2.1加权转移系统是一个元组W =(M,K,θ),其中M是一个非空的状态集,K ={e1,.,e k}是有限资源集,θ是非空作用集,θ:M × θ ×(K→R≥0)→ 2 M是标号转移函数。代替mJ∈ θ(m,a,f),我们写mfmJ,我们称f为权函数。为简单地说,在下面的内容中,我们假设K是一个单例,我们使用转换函数θ:M×(θ×R≥0)→2M.然而,该工作可以直接扩展到包括多个资源,并且所有以下结果在扩展的情况下保持不变。Alternation-Free Weighted Mu-Calculus(WMC)对WTS的属性进行编码,并涉及模态运算符和资源变量,类似于时间逻辑中使用的那些[1,3,17]:(i) [a]型的转移模态,其中a∈ n;(ii) 递归变量的范围在集合X;他们被用来定义同时递归方程来表达最大和最小固定点,在风格[12,13,24];(iii) 在集合V上变化的资源变量;(iv))对于n∈ {≤,≥}和r∈Q≥0,xr型状态模态,它近似于资源变量x∈ V;(v)类型x的重置运算符 对于资源变量。记法:我们使用b和o在集合{≤,≥}上进行范围调整,使得{0,o}={≤,≥}。类似地,我们使用和D在集合{<,>}上进行范围调整,使得{,D}={<,>}。定义2.2 WMC的公式由以下文法定义,对于任意r∈Q≥0,a ∈ N,x∈ V,N∈{≤,≥},X∈ X。L:φ:= x r |¬φ |φ ∨ φ |[a] φ |φ中的x |X.我们还考虑xr和[a]的德摩根矩阵,定义为:Xr=<$(xorr)和a<$φ=<$([a]<$φ)。292K.G. Larsen等人/理论计算机科学电子笔记319(2015)289JJB2= max{X =a∈<$[a]X<$(φ1→xinY}B1是最小方程组,B2是最大方程组.B2依赖于B1.Q给定φ,φ1,...,n∈ L且X1,., Xn∈ X,令φ{φ1/X1,...,对于i = 1. n.如果=(1,.,n)和X =(X1,...,X n),令φ{λ/X}表示φ{λ1/X1,.,n/X n}。在[12,13]之后,我们允许WMC中相互递归方程的最大或最小块的集合定义2.3[公式 区块] 在集合XB上的方程块B={X1,.,两两不同变量的X n }具有两种形式之一- min { E }或max { E },其中E是(相互递归的)方程组,使得对于任何i,j ∈ { 1,.,m},φ i在Xj中是单调的.E:φX1 = φ1,..., X n= φ n如果B= max{E}或B= min{E},则XB的元素分别称为max-变量或min-变量给定前面定义中的方程组E,其对偶为Eφ:φX1=<$φ1{<$X1/X1, . ,<$Xn/Xn},. . . ,Xn=<$φn{<$X1/X1, . ,<$Xn/Xn}如果B=max{E}或B=min{E},则其对偶分别为B=min{E}或B=max{E}。给定块B,公式φ ∈ L依赖于B,如果它涉及XB中的变量。给定两个块B和Bj,使得XB<$XB′=<$,如果B的方程的右边公式依赖于B, 则 称 B 依 赖 于 B j .定义2.4 [无交替块序列] A序列B = B1,...,m≥ 1个两两相异方程块的B m是无交替块序列,(i)XBi<$XBj=,对于i(ii)如果i< j,则B i不依赖于B j。一个公式φ∈ L依赖于B,如果它依赖于序列中的每个块。例2.5预先考虑语义,WMC 中的块序列可用于编码,例如,WCTL的 公式A(φ1U[r,r′]φ2):1etφ=X依赖于无选择序列B=B1,B2,定义如下B1=min{Y=(φ2<$r≤x≤r)<$(φ1<$a∈<$[a]Y)}3WMC的加权语义为了在WTS方面为WMC提供语义,我们定义了资源估值,扩展状态和环境的概念资源估值是一个函数l:V →R≥0,它为V中的资源变量分配(非负)实数。我们用L表示资源估值类。对于l∈L,x∈ V和s∈R≥0,令l[x<$→s]∈L定义为:K.G. Larsen等人/理论计算机科学电子笔记319(2015)289293E(Ⅲ)EE(Ⅲ)ρ[X<$→λ]ρ[X<$→λ]EEEE对于y / = x,l [x<$→s](x)= s和l [x<$→s](y)= l(y);设l + s∈L定义为(l +s)(x)= l(x)+s。给定一个WTSW =(M,λ,θ),m∈M,l∈L,(m,l)称为W的一个扩张态.扩展状态之间的转换定义如下:(m,l)−→a(mJ,lJ)i<$m−→uamJ且lJ=(l+u)。给定WTS W =(M,θ,θ),环境是一个函数ρ:X →2 M×L,它将递归变量解释为扩展状态集。 我们使用0作为空的环境,它将递归变量关联到所有递归变量。给定一个环境ρ和S<$M×L,设ρ[X<$→S]是将X解释为S的环境,所有其他递归变量都像ρ一样。类 似 地,对于成对不相交元组X =( X1,., Xn)∈Xn且S =(S1,.,Sn)<$(M×L)n,设ρ [X <$→S]是将X i解释为Si的环境,对于所有i =1. n和所有其他变量一样。给定一个WTSW =(M,θ,θ)和一个环境ρ,L的WTS语义在布尔逻辑的经典语义之上定义如下。W,(m,l),ρ |= x <$r i <$l(x)<$r;W,(m,l), ρ|=[a]φi∈any(mJ,lJ)∈M×Ls.t.(m,l)−→a(mJ,lJ),W,(mJ,lJ),ρ| = φ;W,(m,l),ρ| = xinφ i <$W,(m,l [x<$→ 0]),ρ |= φ;W,(m,l),ρ| = Xi <$(m,l)∈ ρ(X).设φ ρ={(m,l)∈ M × L |W,(m,l),ρ |= φ}。在[12,13,24]之后,我们现在扩展语义以包括由块的无交替序列施加的限制,并获得所谓的块语义。给定一组方程E,其中变量X =(X1,...,X n),环境ρ和λ =(λ 1,...,<$n)<$(M ×L)n,设函数f ρ:(2 M×L)n−→(2 M×L)n被定义为如下所示f ρ(λ)= λφ1),., (φ n)观察到(2M×L)n形成一个完全格,其排序、连接和相遇操作被定义为集合论包含、并和交叉口。 此外,对于任意的E和ρ,fρ是单调的因此,它有一个最大不动点表示为νX.fρ,一个最小不动点表示为μX.fρ[12]。这些可以被描述为E如下所示:Ev X.f ρ={|f ρ(|f ρ(π)π}。块max{E}和min{E}定义满足E中所有方程的环境; max{E}是最大固定点,min{E}是最小固定点。由块B定义的环境用Bρ表示。给定无交替块序列B = B1,...,B m和环境ρ0,设ρ1, . ,ρm由yρi=<$Bi)ρi−1定义,其中i=1, . ,m. B的语义是294K.G. Larsen等人/理论计算机科学电子笔记319(2015)289(Ⅲ)然后由B)ρ0= ρ m。定义3.1[块语义]给定块的无选择序列B,对于WTSW =(M,θ,m∈M,资源估值l∈L,环境ρ,如下:W,(m,l),ρ| = Bφ i <$W,(m,l),Bρ|= φ。我们说公式φ是B-可满足的,如果在某种资源估值和某种环境下,存在至少一个WTS,对于无选择块序列B的一个状态,满足它; φ是B-有效性,写为|= Bφ,如果在任何资源估值和任何环境下,在任何WTS的所有状态下均满足。4WMC的符号语义考虑一个可以执行三个动作a、b和c的加权系统,并假设我们对系统的以下特性感兴趣1. 它可以做一个a-动作,然后是一个无限序列的非零成本的动作b和c2. 在a-转换之后,整个行为花费少于一个单位的资源。这些需求可以在WMC中编码,通过使用三个资源变量xa,xb和xc,如下所示:φ=a(xainX),B= max{X =xa 1b(xbin(Yxc>0)),Y=xa 1c(xcin(Xxb>0))}我们可以看到,在B的假设下,存在一个满足φ的WTS。 但它不能满足一个有限的WTS,因为它必须有至少一个非零成本转换的无限迹,总成本有界。然而,所有满足φ编码要求的WTS都有一些共同点:资源变量在某些资源估值下的行为方式以及重置的结果。这种观察激发了符号加权转换系统(SWS)的发展,它类似于[2,4,23]中用于时间自动机的系统。这些是WTS的抽象:符号模型是一个标记的转换系统,通过涉及抽象定量信息的区域概念来表示WTS的无限集合。人们可以为WMC提供一个SWS-语义(符号语义),并且可以证明WTS和SWS之间存在一种关系,使得在这种关系中的任何系统都满足相同的WMC属性。此外,关系是完整的,在这个意义上,每个WTS对应一个SWS和反向。这一事实的一个重要后果是,WTS-语义的有效性与SWS-语义的有效性一致对于一个ys∈R≥0,let[s]=max{z∈N |z≤s},{s}=s−[s]且[s|=min{z∈N|z≥ s}。K.G. Larsen等人/理论计算机科学电子笔记319(2015)289295定义4.1给定N∈N,l,lJ∈L与t等价。 N,用l=NlJ表示D我说:1. <$x∈ V,l(x)> Ni<$lJ(x)> N;2. x∈ V s.t. 0 ≤ l(x)≤ N,[l(x)]=[lJ(x)]且{l(x)}= 0惠{lJ(x)}= 0;3. x,y∈Vs. t. 0≤l(x),l(y)≤N,{(l(x)}≤{l(y)}惠{(lJ(x)}≤{lJ(y)}。在= N下的等价类称为N-环. Let[1]是包含l的区域,并且RVN是对于资源变量的集合V和常数N的所有N个区域的集合。 对于一个给定的N∈N,当v er V是有限的时,RVN是有限的。对 于 δ∈RVN, 一 个 子 空 间 是 区 域 δjs.t.对 任意yl∈δ , 存 在 d∈R≥0s.l+d∈δJ , 记 为byδ~δJ。 对于δ∈RVN,x∈V,n∈N,δ[x <$→n]表示存在LJ∈δs. t的所有资源估值l所组成的区域. l = lJ [x→ n]。例4.2在图1中,给出了N= 1和V={xa,xb,xc}。δ0= [xa=xb=xc=0]δ2=[xb=0, 0xa=xc1]<<δ4=[xc=0, 0xbxa1]<<0)),Y=xa 1c(xcin(Xxb>0))}。δ0= [xa=xb=xc=0].δ2= [x b= 0,0< x a=x c<1].regδ=[x=0,0< x< x<[1]t14=({(X,xb>0)},δ4)4cbat13=({xcin(X<$xb>0)},δ7)保留地δ6= [xb= 0, 00)),x >0},δ)modδ1=[00},δ6)res,εt10=({xb in(Y<$xc>0)},δ5)modt9=({x a<1,xb<$(x b in(Y<$x c> 0)),x b> 0},δ4)reg,t8=({(X,xb>0)},δ4)δ5=[00)},δ3)保留地t=({x1,c<$(x in(X<$x >0)),x >0},δ)mod6acbc2reg,t5=({Y,xc>0},δ2)res,t4=({xb in(Y<$xc>0)},δ1)t=({x1,<$b<$(x in(Y<$x >0))},δ)0mod3abCreg,t2=({X},δ0)rest1=({xa inX},δ0)t0=({xa}xa (X)},δ0)mod图二. 表T(φ,B)图3.第三章。φ依赖于B的SWS在图2中示出了T(φ,δ0)。只有一个无限的踪迹-我们构造Ws:εs={a,b,c,εx,εx,εx},εs=εx一一B(t0,δ0)(t3,δ0)(t6,δ1)εxBεxB(t12,δ6)(t12,δ5)(t6,δ2)CBC(t9,δ7)εx(t9,δ4)εx(t9,δ3)CC∧∧300K.G. Larsen等人/理论计算机科学电子笔记319(2015)289{(t0,δ0),(t3,δ0),(t6,δ1),(t6,δ2),(t9,δ3),(t9,δ4),(t12,δ5),aBC(t1 2,δ6),(t9,δ7)}和θs的定义如图3所示。从图3中的系统模型中,可以生成一个WTS,在这种情况下,它是无限的;φ在它的某些状态在图4中显示了这个无限模型的一部分K.G. Larsen等人/理论计算机科学电子笔记319(2015)289301m00上午1时10π Bm2...m3...M410π C...0。2c56l0=(0, 0, 0)l1=(0. 三,零。三,零。3) l2=(0. 三,零,零。第三章l3=(π,π,π)l4=(π,0,π)10 10 10 10 10l5=(0. 1,0。1,0。1)l6=(0. 1 0 0 第一章l7=(0. 五,零。2,0。5)l8=(0. 五,零。(第2、 0段)l9=(0. 3+ ππ03+π)l10=(0. 3+π,π, 0)10 10 10 10 10l11=(0. 三,零。2,0。3)l12=(0. 三,零。(第2、 0段)l13=(0. 六,零。三,零。1)l14=(0. 六,零,零。第一章l15=(0. 五,零。四,零。2)l16=(0. 五,零,零。(二)l17=(0. 75,0。15,0。25)l18=(0. 75,0。(第15条,第 0条)l19=(0. 六,零。1,0。3) l20=(0. 六,零。1、 0)......m0={(t0,δ0,l0)}m1={(t3,δ0,l0)}m2={(t6,δ1,l1),(t6,δ2,l2)}m3={(t6,δ1,l3),(t6,δ2,l4)}m4={(t6,δ1,l5),(t6,δ2,l6)}m5={(t9,δ3,l7),(t9,δ4,l8)}m6={(t9,δ3,l9),(t9,δ4,l10)}m7={(t9,δ3,l11),(t9,δ4,l12)}m8={(t12,δ5,l13),(t12,δ6,l14)}m9={(t12,δ5,l15),(t12,δ6,l16)}m10={(t9,δ7,l17),(t9,δ4,l18)}m11={(t9,δ7,l19),(t9,δ4,l20)}................见图4。 从符号模型不难证明它是φ的模型。Q定理6.4(B -可满足性的判定性)对于任意无选择块序列B,WMC的B-可满足性问题对于WTS-语义和SWS-语义都是可判定的。7公理化在这一节中,我们重点发展一个健全的和完整的公理化的有效性WMC方面的两个语义。 回想一下,这两组有效性是一致的。根据定理5.1,找到SWS-语义的这样一个公理化是足够的,那么它对于WTS-语义也是可靠和完备的。7.1声音公理化为了陈述WMC的公理,我们需要建立一些符号。• 模态前缀是在以下模态算子的字母表上的词w∈ModL,Mod={[a]|a∈n} n{xin|x∈V}。例如,在一个示例中, [a], xin[a][a], [a]xin ,ε∈Modε.8M10男性11例M...M....M7...0。1B.0。2BM....M9...0。15C0。1 C302K.G. Larsen等人/理论计算机科学电子笔记319(2015)289• 上下文C是由模态前缀w∈Mod与元变量X连接形成的词;例如,[a]X,[a]xin[b]X,xin[a][a]X,[a]xinX是上下文。为了强调元变量的存在,我们将使用C[X]类型的函数表示来表示上下文;这将允许我们使用K.G. Larsen等人/理论计算机科学电子笔记319(2015)289303Oo ooL的元素 。例如, 在一个示 例中,如果 C[X] = [a]xin[b]X 是一个 上下文, 则C[(x≥r)] = [a]xin[b](x≥r)∈ L.[1]是一个空的上下文,对于φ∈ L,ε[φ]=φ。WMC的公理化分两个阶段给出。首先,我们提供公理推导的有效性,不依赖于序列的块;其次,我们扩展的公理化递归结构。表2中给出的公理和规则与命题逻辑的公理和规则一起将WMC的非递归有效性的经典演绎关系(见[16])公理化为由R1表示的。对于任意φ,λ∈ L,r,s∈Q≥0,a∈λ,x,y∈ V和任意上下文C [X],给出了公理和规则,其中{0,0}={≤,≥}。(A1):x≥0(A8):xinxinφ→xinφ(A2):(x≥r)(x≤r)(A9):xinyinφ→yinxinφ(A3):<$x≤r→ <$(x≥s),r s(A10):<$<$<$(xinφ)Partixin<$φ(A4):<$x≥r→[a](x≥r)(A11):<$xinφ→(x= 0→φ)(A5):<$x≥r<$y≥s→[a](x≥r+t→y≥s+t)(R1):如果<$φ,则<$φ(A6): (φ→)→(φ→)(R2):{C[x<$r]|rDs}C[xs](A7):在R3中的X→X(R3):{C[x≥r]|r∈Q≥0}<$C[<$]WMC基本公式公理(A1)-(A3)陈述简单的算术事实。(A4)说明一个动作转换有一个正的成本。(A5)保证所有的资源变量表示相同的资源。公理(A6)和规则(R1)指出WMC的所有盒状算子在模态逻辑意义下是正规的[8]。复位操作的性质由(A7)-(A11)描述规则(R2)和(R3)是无穷的,并且编码了有理数的阿基米德性质例如,公式{(≥r)|r
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- 深入理解23种设计模式
- 制作与调试:声控开关电路详解
- 腾讯2008年软件开发笔试题解析
- WebService开发指南:从入门到精通
- 栈数据结构实现的密码设置算法
- 提升逻辑与英语能力:揭秘IBM笔试核心词汇及题型
- SOPC技术探索:理论与实践
- 计算图中节点介数中心性的函数
- 电子元器件详解:电阻、电容、电感与传感器
- MIT经典:统计自然语言处理基础
- CMD命令大全详解与实用指南
- 数据结构复习重点:逻辑结构与存储结构
- ACM算法必读书籍推荐:权威指南与实战解析
- Ubuntu命令行与终端:从Shell到rxvt-unicode
- 深入理解VC_MFC编程:窗口、类、消息处理与绘图
- AT89S52单片机实现的温湿度智能检测与控制系统
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功