没有合适的资源?快使用搜索试试~ 我知道了~
可在www.sciencedirect.com在线获取理论计算机科学电子笔记290(2012)19-36www.elsevier.com/locate/entcs基于重写的线性时态逻辑模型的KyungminBae1Jos'eMeseguer2美国伊利诺伊大学厄巴纳-香槟分校计算机科学系摘要本文提出了一个模型检查器的LTLR,一个子集的时间逻辑重写TLR扩展线性时间逻辑与空间动作模式。LTLR和TLR是非常有表现力的逻辑,它是对著名的基于状态和基于动作的逻辑的概括。进一步,根据重写理论给出了TLR-LRR的语义,从而对LTLR性质进行了模型检验可以通过重写规则在非常高的级别上指定。 本文回答了一个不平凡的挑战,即,通过重用Maude的重写理论LTL模型检查器,能够构建一个模型检查器来对重写理论上的LTLR为此,重写逻辑及其Maude实现的响应特性已被证明非常有用。关键词:重写时序逻辑,模型检测,重写逻辑,响应变换1引言在时态逻辑和模型检查中,可以区分两个主要阵营:基于状态的阵营,其中公式中的所有原子都是状态谓词(例如, LTL、CTL和CTLcamp[11]);以及基于事件的camp,其中公式Hennesy-Milner在语义层次上,基于状态的公式在Kripke结构上进行评估。相反,基于动作的公式在标记的转换系统上进行评估有些性质可以在基于状态的逻辑中自然地表达,而在基于动作的逻辑中很难表达,而其他性质的情况则相反。这意味着,当属性不适合给定的逻辑时,必须1电子邮件:kbae4@cs.uiuc.edu2电子邮件:meseguer@cs.uiuc.edu1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2012.11.00920K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19属性,以便在给定逻辑中对其进行模型检查。对于混合属性,例如公平属性(参见讨论[31]),情况更具挑战性,其中涉及基于状态的谓词和动作关于这种情况,我们可以说,如在[31]中,串联,每个由一对LS/LP给出,其中LS是指定系统的形式主义(例如,Kripke结构或标签转移系统的形式主义),LP是描述属性的形式主义(例如,一些基于状态或基于动作的时态逻辑)。在基于状态和基于动作的串联中,经常需要1.1一个例子为了说明缺乏表达性,无论是完全基于状态还是完全基于动作的系统,我们使用一种简单并行语言的变体,其重写语义在[15,18]中给出,其中我们可以定义Dekker并行语言支持在共享内存机器上并发执行的进程,并通过共享变量相互Dekker的算法有两个进程,代码完全对称。 进程1将布尔变量c1设置为1,以指示它希望进入其临界区。过程2对变量c2做同样的事情。如果一个过程在将其变量设置为1后发现其竞争者的变量为0,那么它立即进入临界区。在平局的情况下(两个变量都设置为1),使用在{1,2}中取值的变量turn来打破平局。例如,进程1的代码如下:重复’c1当ifwhileFiod;暴击;其中用于程序的临界部分和剩余部分的代码片段分别被抽象为常数CRIT和REM3。全局状态被建模为对,第一个组件是一组进程,第二个组件是共享内存。在他们的Maude重写语义中,这样的全局状态是模式{[I,R]|S ,M},其中[I,R]是进程,其中I是进程ID,R是接下来通过处理,|是关联-交换并行进程合成算子,S是进程的剩余集合,M是共享内存。语言[3]我们假设暴击是终止的,但REM可能不是。见[15]的“熟”版本的例子,和[ 1 ]的Maude规范的例子和LTLR属性。K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1921Dekker算法的一个要检查的属性(实际上它失败了,见第5QQ执行官p1,QQ评论员p1.-crit.p1中的谓词意味着过程1处于其临界区,并且可以通过以下等式{[p1,crit; R] |S,M}|= in-crit.p 1 = true。然而,上面的强公平性公式只是为了表达exec.p1,我们需要在这个“烹饪”之后{[I,R]|S,M,p1}|= exec.p 1 = true。这只是一种复杂的方式,将真正的操作(exec.p1)直接表示为状态谓词。同样,在基于状态的系统中也有一些自然属性需要一个复杂的“烹饪”来表示为动作。例如,当过程处于其rem部分时为真的谓词,比如说-rem.p1,在基于动作的系统中定义是不平凡的,而在基于状态的系统中通过类似于in-crit.p1的方程在本文中,我们描述了一个新的串联重写逻辑/TLR的,第一次提出在[31]中,烹饪系统和财产的需要消失了。例如,上述用于Dekker的强公平性公式可以直接用TLR公式表示。我们还提出了一个基于Maude的模型检查器的LTLR子逻辑的TLR的扩展与行动的LTL逻辑。关键是重写逻辑[30]比Kripke结构和标记转换系统更有表现力逻辑TLR的重写,称为时间逻辑,扩展CTL的重写空间动作模式,这是非常有表现力的,因为它们可以本地化一个重写规则的动作到一个给定的在 本 文 中 回 答 的 非 平 凡 的 挑 战 是 能 够 建 立 一 个 模 型 检 查 器RewritingLogic/LTLR串联相对较少的e-terrorort通过重用Maude为此,重写逻辑及其Maude实现[15]的相应特性已被证明是非常有用的。本质上,新的模型检查器设计使用[31]中的结果,通过该结果,重写理论R上的LTLR公式的模型检查可以简化为翻译的Kripke结构上的翻译的LTL公式的模型检查使用反射,这在这里通过将每个重写理论R与新理论相关联的反射理论变换来实现,使得给定的LTLR公式对于R和给定的初始状态成立,当且仅当其LTL平移对于新理论成立本文的结构如下。第2节介绍必要的背景22K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19|第3节提供了形式基础,定义并证明了相应结构的正确性。第四节在此基础上给出了LTLR模型检测器的相应设计。第5节通过一个例子说明了模型检查器的使用;第6节讨论了相关的工作并给出了结论。2重写逻辑与重写的时间逻辑本节解释了RewritingLogic和TLR检查器的概念,构成了RewritingLogic/TLR检查器串联,这是本文描述的模型检查器的语义基础设施。2.1重写逻辑重写理论是一个具有静态状态和状态之间并发转换的并发系统的形式化规范。更确切地说,重写理论是三元组R=(E,E,R)4,使得:• (E,E)是一个多分类的方程理论。[5]由方程理论(E,E)定义的初始代数T/E定义了由R指定的系统的状态。• R是重写规则的集合,形式为l:q−→r,l是标签(可以为多个规则复制),q和r是相同种类的项,并且变量vars(r)的集合是变量vars(q)的子集。这些重写规则定义了状态之间的并发转换。更准确地说,每个状态被建模为基项的E-等价类[t] E,并且重写以E为模发生;也就是说,重写E-等价类[t] E表示状态,而不仅仅是项t。在R i中存在一个一步重写[t]E−→R[t]E,其中存在u ∈ [t] E,使得u可以使用标准w a y中R中的某个规则l:q −→ r重写为v,6记为u−→Rv,并且w e还具有v e v∈[t]E。最有用的重写理论满足额外的可执行性条件,例如:因为对于任意的E和R,无论[t]E−→[1]一般情况下,E是不可预测的。一重写理论R=(E,E)RA,R)是可计算的,如果下列条件成立:(i) 模A相等是可判定的,并且存在模A匹配算法,产生有限数量的A-匹配替换或失败,可以在A-等价类中实现重写(ii) (,EA)是接地端接和连续模A[16]。 也就是说:(i)不存在E模A的无限重 写 序 列 ; ( ii ) 对 于 每 个 [t]A∈T<$/A , 存 在 唯 一 的 A- 等 价 类 [canE/A(t)]A∈T<$/A,称为[4]这个定义可以扩展到[3,15]中更一般的重写理论,它使用了更具表达力的等式逻辑,条件重写规则和冻结函数运算符。[5]方程理论(E1,E2)有各种可能性,如无序、多序、序,甚至成员关系方程逻辑。然而,为了使阐述尽可能简单,我们将假设(E,E)是一个多分类的方程理论。[6]参见[16]关于项重写的基本符号。术语中的位置被表示为非零自然数的字符串,并且当术语被解析为树时表示树位置 两个有用的概念是给定项t在给定位置p处的子项,记为t p,以及在t中用位置p处的另一项u替换这样的子项,记为t[u]p。例如,在项t = x+((z +0)+y)中,位置2处的子项。1是z+0,而n是t[z]2。1是项x+(z+y)。K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1923^|[t]A模A的E-标准形式,使得任何以[t]A开始的终止序列的最后一项(不能用E模A进一步重写)必然是[canE/A(t)]A。(iii) 规则R相对于方程E模A是基本相干的[37]。也就是说,如果[t]A通 过R中的规则l重写为[t]A, 则[canE/A(t)]A也通过相同的规则l重写为[t]A,使得[canE/A(t)]A=[canE/A(t)]A此外,为了使重写逻辑和TLR重写的集成更平滑,我们定义重写理论的类RWTh0如下。定义2.1当满足以下条件时,R ∈RWTh0• R是可计算的,并且有一个sortState作为其选择的状态。• 如果R有一个名为Prop的排序,那么它也必须有一个名为Bool的排序,其中包含常量true和false,以及一个运算符 |=:状态×属性→布尔值。7• 它 的 状 态 谓 词 符 号 的 子 签 名 是 中 所 有 形 式 为 p 的 算 子 的 集 合 :A1× · ·· ×An→Prop,n≥0。A1,...,n称为原子状态谓词p的参数排序。• R是无死锁的,也就是说,没有有限序列[t1] A−→ R[t2] A. [tn]A−→R[tn+1]A使得[tn+1]A不能被进一步重写(即,它是“死锁状态”)。这根本不是一个强限制,因为如[15,33]中所解释的,任何重写理论R,其规则在其条件中没有重写,都可以转换为语义等价的无死锁理论R。证明项和计算重写逻辑的推理规则推导出由R[3,30]指定的系统中的所有并发计算。 也就是说,给定两个状态[u],[v]∈T<$/E<$A,可以通过一些可能复杂的并发计算从[u]到达[v],当且仅当可以证明R<$[u] −→+[v]8。在重写逻辑中,任何这样的从[u]到达[v]的复杂计算都由证明项[30,31]证明,比如λ,写作R <$λ:[u] −→+[v]。证明项是被识别的模自然方程,使得任何证明项λ始终等同于交织描述,作为顺序组合γ1;… ; γ k的一步证明项γ i[3,30,31],它有一个非常简单的代数描述。定义2.2给定重写证明R<$γ:[u]−→R[v]使用重写规则l:q−→r∈R,一步证明项γ具有形式t [l(φ)] p,其中t∈ [u],p是 t中应用该规则的位置,并且φ={x1<$→u1,.,x n<$→u n}是一个置换,使得t|p= φ(q),t [φ(r)] p∈ [v],其中x1,., x n是q 中 的 变量。在上面的定义中,如果t是一个E/A-正则项,比如t = canE/A(u),我们说canE/A(u)[l(φ)] p是一个正则的一步证明项[31]。规范一步法7Prop是原子状态谓词的指定类型,而=是定义给定状态是否满足给定状态谓词的函数。8[u]-→+[v]表示并发重写的一个或多个顺序合成的组合。24K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19γ(n)重写证明是达到我们所期望的计算概念的关键因素,在此基础上将评估TLR在定义计算之前,让我们定义两组有用的规范证明项。第一,所有形式为[canE/A(t)]A的A-等价类的集合(Can E/E,A)State,其中t是SortState的基项。其次,我们可以定义R中所有一步规范证明项的集合CanPTerms1(R)。在可计算重写理论中,任何证明项在语义上总是等价于规范项[31]。定 义 2.3R ∈RWTh0 中 的 无 限 计 算 是 一 对 函 数 ( π , γ ) , 其 中 π : N−→(Can_n/E,A)态和γ:N−→Can_p_terms1(R)使得对于所有n∈N,π(n)−→π(n + 1)是R中的规范一步重写证明。从图形上看,γ(0)γ(1)γ(n)π(0)−→ π(1)−→ π(2). π(n)−→ π(n +1).Comp(R)∞表示R中的无限计算的集合,并且对于每个[t]∈(Can/E,A)状态,Comp(R)∞[t]表示从[t]开始的无限计算,即那些计算(π,γ)使得π(0)=[t]。给定一个无限次计算(π,γ)和一个数i∈N,(π,γ)i表示(π,γ)的从位置i开始的子集x,即函数对(πsi,γsi),其中s是后继函数,s0是恒等函数,sn+1=ssn。空间动作空间动作是TLR的动作原子。他们概括了一步证明条款,这可以被认为是地面实例化的空间行动。空间作用描述的模式,一般不只是指定一个单一的一步证明项,但可能是无限的一组这样的证明项。粗略地说,我们可以把空间动作看作是设Ω是构造函数9的子签名,L是R中标记规则的标签集,并假设Ω<$L=<$。签名Ω(L)通过以下方式扩展Ω:• 新鲜的排序顶部和Subst• 结合和交换算子_;_:Subst Subst→Subst。• 对于每个重写规则l:q−→r在R中,其中q,r为B类,并且具有变量x1,.,x n在q中具有排序B1,., B n:· 运算符l:Subst→B和x1\_:B1→Subst,...,x n\_:B n→Subst· 一个B类的常数l和一个运算符top:B→Top,设X是一个多排序的变量集,对于Ω中的每一种排序,都有一个无穷多的变量集。考虑代数:(i)变量在X中的Ω(L)-项的A-等价类的TΩ(L)/A(X);(ii)变量在X中的Ω-项的A-等价类的TΩ/A(X)。此外,假设代入φ具有形式x1\u1;···;xn\unn。9Ω Ω是与接地连接和终止(模)相关的构造函数的子签名A) 理论(ε,E<$A),其中f∈Ω i <$,有一个基项ts.t.f是[canE/A(t)]中的函数符号K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1925定义2.4R• 对于每个l∈L,[l]A,[top(l)]A∈SP(Ω,L)• [l(φ)] A∈ SP(Ω,L)如果l ∈ L,[l(φ)] A∈ TΩ(L)/A(X),u1,., un∈ TΩ/A(X)• [top(l(φ))] A∈SP(Ω,L)如果l∈L,[top(l(φ))] A∈TΩ(L)/A(X),u1,.,un∈ TΩ/A(X)• [v[l]p]A∈SP(Ω,L)如果p不是空(顶)位置,l∈L,[v[l]p]A∈TΩ(L)/A(X),且v∈TΩ/A(X).• [v [l(φ)] p] A∈SP(Ω,L)如果p不是空(顶)位置,l∈L,[v [l(φ)] p] A∈TΩ(L)/A(X),且v,u1,.,un∈ TΩ/A(X).SP(Ω,L)定义空间动作模式的Ω(L)项。注意CanPTerms1(R)<$SP(Ω,L),因此任何规范的一步证明项都是某个空间动作模式的基础版本。形式为l的操作模式描述了一个标记为l的规则,该规则可以应用于任何地方。动作模式l(φ)允许l也被应用于任何地方,但是将与规则l相关的变量实例化约束为自身是φ的另一个实例。需要top(l(φ))形式的动作模式来覆盖l应用于术语顶部的情况。最完整的空间模式是形式v[l(φ)]p的模式,其中v是非空上下文,p是位置。空间动作模式和证明项之间的实例关系捕获了空间动作模式的这些含义。设[u]A≤A[v]A i ≠ 0,存在一个多序置换θ使得[u]A= [θ(v)]A10。另外,对于替换项,我们定义[φ]A≤A[vi]A i ∈[ v i ]A,存在[xi\ui]A∈[φ]A使得[ui]A≤A[vi]A。定义2.5规范的一步证明项γ和空间动作模式δ∈SP(Ω,L)之间的实例关系,记为γ±Aδ,是≤A关系的一个微小变体,定义如下:• [v[l(φ)]p]A±A[l]A• [v[l(φ)]p]A±A[l(φ)]A i <$[φ]A≤A[<$]A• [v[l(φ)]p]A±A[w[l]p<$]Ai <$[v[l()]p]A≤A[w[l()]p<$]A• [v[l(φ)]p]A±A[w[l(φ)]p<$]Ai <$[v[l(φ)]p]A≤A[w[l( φ)]p<$]Aand[φ]A≤A[<$]A• [l(φ)]A±A[top(l)]A• [l(φ)]A±A[top(l(φ))]A i <$[φ]A≤A[<$]A.反射与元级计算重写逻辑是以精确的数学方式反应的[12],即,是一个有限呈现的重写理论U,它是普适的,因为我们可以在U中将任何有限呈现的重写理论R(包括U本身)表示为项R,将R中的一个yt e rmst,t ti表示为项t,ti,并且将一个y对(R,t)表示为t e rmiR,ti,这样我们就具有以下等价性Rt−→t惠UR,t−→R,t10这是一个可判定的关系,我们假设存在A-匹配算法26K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19由于U本身是可表示的,我们可以实现具有任意数量的反射水平的Rt→t惠UR,t→R,t惠UU,R,t→U,R,t.. .普适理论U的关键功能可以由下降函数控制[15,14]。例如,在Maude中,给定R=(R,E<$A,R),U的几个关键结构由以下下降函数定义:• MetaReduce(R,t)元表示R中项t的E/A-标准形式。 如果R是可计算的,那么[t]E/A=[t]E/Ai=MetaReduce(R,t)=MetaReduce(R,t)。• 元匹配(R,t,t)元表示两项之间的模A的实例关系:t≤A元匹配(R,t,t)=t.• metaXapply(R,t,l,m)11meta表示R中规则l对项t的第m次一步重写。R[v [l(φ)] p] A:t→tim s.t. metaXapply(R,t,l,m)=(t_p ,v[]p,φ).2.2重写的线性时间逻辑TLR是一个由空间作用SP(Ω,L)和原子命题的签名参数化的逻辑族。这些逻辑中最通用的是TLR逻辑,它是基于状态的CTL逻辑的通用化,允许公式中的空间动作和状态谓词。它包含了各种重要的子逻辑,这些子逻辑作为特殊情况出现(见[31])。为了我们在这里的模型检查目的,我们有兴趣扩展[15]中描述的用于重写理论的MaudeLTL模型检查器对空间动作的支持,我们关注LTLR,子逻辑生成LTL,它通过空间动作SP(Ω,L)和状态谓词的签名被参数化为LTLR(SP(Ω,L),Ω)下面是类似于BNF风格的LTLR的语法,其中,我们采用隐式通用路径量化的LTL符号12,而不是使用类似于CTL的符号:δ:SP(Ω,L),p:Prop(Ω),λ,λ:LTLR(SP(Ω,L),λ)LTLR(SP(Ω,L),Ω):δ|p|¬ϕ|ϕ∨ϕ∗|ϕ∧ϕ∗|Ⓧϕ|ϕUϕ∗|ϕRϕ∗|ϕWϕ∗|Q|Q通过限制所允许的原子命题和/或空间作用,可以得到TLR_n(SP(Ω,L),_n)的更小的有用的子逻辑.也就是说,我们可以定义由空间作用的子集WSP(Ω,L)和原子命题的子集ΔProp(Ω)参数化的TLR的具体地,子逻辑LTLR(W,Δ)<$LTLR(SP(Ω,L),<$)由集合理论公式LTLR(W,Δ)={<$∈LTLR(SP(Ω,L),<$)|其中sp(n)表示n的空间作用子公式的集合,而prop(n)表示原子位置子公式的集合. 特别地,当W=π,并且Δ =Prop(Π)时,我们获得了基于状态的逻辑LTL的专门化;即,[11] meta Xapply的这个定义只描述了实际函数的一部分。 [15]见《无量寿经》。[12]我们假设所有的状态谓词常量和函数符号都是构造函数,即, 有一个子签名包含Ω,然后将原子命题的集合Prop(n)定义为基础项Prop(Ω)=TΩProp。K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1927LTL(λ)=LTLR(λ,λ)。 F或其他类似的专业化到各种基于状态和基于动作的逻辑,见[31]。满足关系R,[ t ]给出了公式<$∈LTLR(SP(Ω,L),<$)的语义|其中R∈RWTh0具有构造器Ω和状态谓词Ω的子签名,并且[t]是状态(即,一个A-等价类[t]A在E-标准型模A和排序状态,其中E<$A是方程,R)。根据定义,R,[t]|当且仅当对于每个无限次计算(π,γ)∈Com p(R)∞[t],路径满足关系R,(π,γ)|=holds。 因为一个人可以用SP(Ω,L)、Prop(L)和基本连接词T、<$、、U来表达所有的LTLR(SP(Ω,L),),所以定义原子和这些连接词的语义就足够了。由于LTLR概括了LTL,其语义定义与LTL的语义定义完全相似(参见,例如,[27])。关键的新增加是空间动作的语义;关系R,(π,γ)|= δ成立当且仅当当前计算的证明项γ(0)是空间动作模式δ的实例。路径满足关系归纳定义如下:• R,(π,γ)|= T• R,(π,γ)|= p惠canE/A(π(0)|= p)= true• R,(π,γ)|= δ⇔γ(0)±Aδ• R,(π,γ)|=<$F R,(π,γ)|=• R,(π,γ)|= π,γ,R,(π,γ)|= π或R,(π,γ)|=• R,(π,γ)|=100%(π,γ)|=• R,(π,γ)|= U惠k ∈ N s.t. R,(π,γ)k|= 0 ≤ i (W,<$),我们可以将其映射为以下公式通过系统地替换空间动作的每次出现,δ∈W,由公式Xδ表示。结构KW(R),加上上面的公式translation(),定义了一个串联映射(KW,()):重写逻辑/TLR(W,)−→克里普克/CTL(Kripke,W)。该映射是保持满足关系的串联的忠实|=CTL(CTL W)中的CTL。|= CTL∗ in CTL∗ (Π ∪ W). 这一点可以从以下几个方面看出来Orem在[31]中详细证明,其中还给出了约化的复杂性理论分析定理3.3给定重写理论R ∈RWTh0和有限个W<$SP(Ω,L),对于R,U<$W和<$∈TLR< $(W,L)中的每个状态[t],以下等价成立:R,[t]|= KW(R),([t],U)|= CTL密码3.2作为回应性理论转换的K-WKW(R)构造将RWTh0中的每个重写理论映射到Kripke结构。然而,正如[31]中所指出的,分解映射R<$→[13]由于任何TLR公式都只涉及空间作用的有限集合sp(W)作为子公式,所以考虑TLR公式中的公式总是足够的,W是有限的。[14]回想一下,原子命题集合AP上的Kripke结构是三元组K=(A,R,L),其中A是状态集合,R<$A×A是全转移关系,L:A−→ P(AP)是一个标签函数,将在a中成立的原子命题集合L(a)<$AP赋给每个状态a∈A。K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1929RKW(R)改写成RW后的理论变换R R的一般构造R <$→ K(R),在[15,18]中详细阐述,它将每个RWTh0映射到其底层的Kripke结构。也就是说,我们可以将KW(R)结构分解为KW(R)=K(RW)。这对于工具构建的目的特别有用,因为构造R ›→ K(R)已经在Maude的LTL模型检查器中自动化了[15 ]第10段。所以,“本质上”我们需要做的就是自动化理论转换R ›→RW。在这里,2.1节中总结的重写逻辑的相关属性变得非常有用,并且在Maude中得到了META-LEVEL模块的有力支持在下文中,我们详细描述并证明了R›→RW变换的一个相应的参数构造是正确的,其中参数 R元表示为通用重写理论U中的项R。然后,我们可以得到R→RW构造作为相应的参数重写理论U(),当用参数W和R实例化时,产生扩展U的理论UW(R),并提供理论RW的正确实现。我们在下面详细解释参数UW(R)构造。特别要注意的是,UW(R)结构必须元表示一步证明项和空间动作模式之间的实例关系±A在U的排序和下降函数的META-LEVEL内置实现由于元匹配在每个重写理论上都是参数化的,因此其元表示在给定重写理论上也是参数化的让±表示与第二节中的重写理论R=(Ω,E<$A,R)相关联的方程理论(Ω(L),A)中的一步证明项和空间动作模式的元表示之间的实例关系的元表示2.1.然后,对于一步证明项γ和空间动作模式δ,我们有γ±Aδi ∈γ±(Ω(L),A)δ. UW(R)构造包含了普适理论U,因此可以定义如下。定义3.4重写理论UW(R)是普适理论U的如下参数扩展,其中R=(Ω,E<$A,R)和W<$SP(Ω,L)被元表示为数据参数R和W:• U UW(R),其中UW(R)包括元级中的模以及关系γ±(Ω(L),A)δ的下降函数。• UW(R)具有带有常量true和false的sort State、Prop和Bool,其中sort State的基础项是pairs(t,U),其中t是sort State中的项,R和UW(也就是说,U是一个元项,它使用一个集并结合和交换运算符来表示W中包含的有限个动作模式集)。•UW(R)也有一个作用算子,使得act(W,γ)={δ∈W|γ± Rδ}。• 在 UW ( R ) 中 存 在 单 个 条 件 重 写 规 则 tr , 使 得 tr : ( t , U ) -→(metaReduce(R,t),V)i,其中在R中存在规则la b el l和自然numbermsuch,其中metaXapply(R,t,l,m)=(tt,v[]p,φ)<$V=ac t(W ,v[l(φ)] p)。 规则的条件可以用带有额外变量的“匹配条件”用等式表示(参见[ 15 ])。注意,特别是这意味着我们有一个单步重写证明项R <$v[l(φ)]p:t−→t<$。30K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19˜˜˜• 类Prop的基项正好是以下项的元表示:(i)R的原子命题,或者(ii)W的元素。• 有一个标签操作符|=:状态×Prop→布尔,条件方程为:· (t,U)|=δ= true i δ∈ U· (t,U)|= p = true i {metaReduce(R,t |= p)=真,即, 罐E/A(t |= p)= true。上面定义的理论UW(R)是对KW(R)的元级描述,因此该定义与定义3.1密切相关。UW(R)结构的正确性命题3.5给定重写理论R∈RWTh0和有限集合W∈SP(Ω,L),对于R和U中的每个状态[t],以下条件成立:(i) K W(R)的状态([t],U)与U W(R ) 中的(canE/A(t),U)形式的基项Sort状态一一对应。(ii) 对于KW(R),([t],U)的每个原子命题α,|= α i(canE/A(t),U)|=在UW(R)中,α =真。(iii) 在KW(R)i <$$>中有一个跃迁([t],U)−→<$([t<$],V)UW(R)<$(canE/A(t),U)−→(canE/A(t<$),V).草图(Sketch)(i) 通过构造,扩展U的反射理论UW(R)中的类态项是KW(R)的元表示态对(canE/A(t),U)([t],U).这种元表示是一对一的,因为关于R的可计算性假设(包括E模A的连续性和终止性)。(ii) 有两种情况,当([t],U)|= α在KW(R)中为真; α∈U,或可以E/A([t])|= α)= true。由于α∈U i <$α∈U且可以E/A([t])|= α)= truei_metaReduce(R,canE/A(t)|= α)=真,在两种情况下,根据上述定义,([t],U)|= α i(canE/A(t),U)|= α。(iii) 如果KW(R)中存在跃迁([t],U)−→([t],V),则根据定义,γ存在一步重写[t]−→[t]在R和V中 =动作W(U)。 但是,定义UW(R),这相当于存在一步重写tr:(t,U)−→(metaReduce(R,t),V),当且仅当R中存在规则标签l和自然数m使得metaXapply(R,t,l,m)=(t,v[]p,φ)且V=ac t(W ,v[l(φ)]p)时,才可能发生。Q除了UW(R)构造外,我们还需要处理与LTLR公式相关的LTL公式的元表示问题定义3.6给定一个公式,除了每个原子命题(分别为空间动作模式)被其元表示替换K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)1931˜4一种LTLR模型的响应式设计Maude支持任何可计算重写理论R [15,18]的基于重写的LTL模型检查,也就是说,Maude自动化了R›→ K(R)构造,并为底层Kripke结构K(R)提供了LTL模型检查器。因此,由于第3.2节中描述的相应U W(R)构造,可以使用第3.1节中描述的将LTLR公式的模型检查简化为LTL公式的模型检查的简化方法,以将R关于公式U∈LTLR(W,R)的模型检查简化为对重写理论UW(R)关于公式U ∈ LTLR(W,R)执行LTL模型检查。然而,在一个实际的模型检查系统实现中,我们希望对用户隐藏所有的元级表示;因此,相应的UW(R)虽然是模型检查器的核心,但并不是用户直接与之交互的对象。 特别是,我们应该支持模型检查命令,其中LTLR公式和初始状态在对象级别指定。这就要求除了执行实际模型检查的内部响应命令之外,还需要设计一个合适的用户界面。正如我们在本节中所解释的,所有这些都可以通过使用响应方法扩展Full Maude语言[17]来实现。4.1基于空间行为模式的LTLR模型构建在LTLR语法中,公式中的原子命题和空间动作模式是不固定的:它们参数化地依赖于给定的可计算重写理论R。特别是,一旦R被指定,空间动作模式就可以被唯一地表征。其思想是,给定R=(E,E,R),具有构造器Ω的子签名和规则标签L,我们可以定义一个映射TLR:R−→RSP(Ω,L),这个地图可以用一个方程定义的函数来元表示TLR:R−→ RSP(Ω,L)在META-LEVEL模块的扩展中。函数TLR可以集成到Full Maude [17]中,通过扩展Full Maude 剩下的事情我们需要做的是定义SP(Ω,L)作为重写理论。 它这并不难,因为我们可以使用Ω(L)的定义和定义2.4。稍微棘手的部分是使作用量v[l(φ)]p只包含一个基本作用量项l(φ)。通过添加运算符将其存档o:Action-A1×A2×A3×···×An →Action-Ao:A1×Action-A2×A3×···×An →Action-A...o:A1×A2×···×An−1×Action-An→Action-A对每个算子o:A1× · ·· ×An→A∈Ω,其中n≥1,其中Action-Ai是每个排序Ai的相关作用排序.由于要产生空间动作模式,32K. Bae,J.Meseguer/Electronic Notes in Theoretical Computer Science 290(2012)19˜在Ω中只能有一个作用子模式,一个基本作用项的唯一性l(φ)作为子项是自动保证的。4.2相应的LTLR模型设计给定一个可计算重写理论R ∈RWTh0,我们现在能够使用TLR(R)来定义LTLR性质,其中是R中的原子命题集。下一步是将LTLR属性转换为LTL属性。 来实现通过与定义3.6相关的公式→定义3.6,可以通过使用元表示理论TLR(R)的反射。 当用户给出扩展到LTLRModel System的Full Maude命令(tlrcheck(t,t).)该系统执行以下任务:(i)解析和元表示t和作为t和t;(ii)计算集合W=sp(t),并且平移t→t是执行;(iii)MaudeLTL模型检查器在理论UW(R)与初始状态(t,τ)和LTL的mula;和(iv)输出的模型检查的结果(真或反例)使用Full Maude的元漂亮打印功能在对象级别提供给用户通过第3节中的结果,我们可以保证(假设Maude和FullMaude实现以及相应的模型检查器实现是正确的)模型检查器系统将对模型检查命令回答true(tlrch
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)