论文研究-逻辑LTS预备模拟关系的判定算法.pdf

所需积分/C币:6 2019-09-11 06:06:44 622KB .PDF
收藏 收藏
举报

进程代数与时序逻辑是并发理论中应用最为广泛的两大规范系统。近来,Gerald Luttgen等人将二者进行结合,提出了逻辑标记转换系统以及相应的精化关系——LLTS预备模拟。提出了一种LLTS预备模拟关系的等价描述方式——泛化预备模拟,并从划分对的角度出发,给出与该描述等价的稳定划分对概念。基于这一概念给出一种判定两个逻辑标记转换系统之间是否具有LLTS预备模拟关系的理论算法,并证明其正确性。
朱文涛:逻辑ITS预备模拟关系的判定算法 2016,52(17)43 B'∈∑使得(A,B)∈T且AsA,B≌B 最后由≤的传递性易得7仍具有传递性。因此 令<,R>,<∑,>为G的两个划分对,则<,RT是一个偏序。 ∑,>(<I,R>是<Σ,T>的精化)当且仅当比∑ 引理3( expand的单性)若≤1s≤2,则 ecpan(≤)E 精细且R∈T()。 令GP,→,F>为个状态有限的LLTS,以 证明设≤1三≤2。令 expand(≤1)=<,R1> PP(G)表示G的所有划分对构成的集合;P上的所有 pand(≤2)=<H2,R2>。下面证明1比2精细且 元关系构成的集合则川RelG)表示。在不致引起混淆 R1sR2(1)。 时分別将二者简记为PP与Rel。 下面给出两数 reduct的定义,该函数从一个划分对 (1比n2精细)设p∈A1∈1且p∈A2∈2。令 出发,构造出一个二元关系 9∈A1,则由1的构造可知p≤1q≤p。因为≤1s≤ 定义5( reduct函数)对于有限 LLTSG的划分对所以p29≤2,从而由m2的构造可知4∈12°于是 <∑,7>,函数 reduct(<∑,7>)按如下方式定义: A1A2,即n比m2精细。 rede;(<∑,T>)={(p,q)3(A,B)∈T(p∈A,q∈B)} (R1≌R2(1)设(B,C1)∈R1。所以,存在rEB1,S∈ 引理1( reduct的单调性)若<n,R><E,T>,则G使得rss。由≤1s2得r2,即存在B2C2∈2 reduca(<H,R>) reduc.(<∑,7>)。 使得r∈B2s∈C2且(B2C2)∈R2。由于比2精 证明设<I,R>匚<∑,T>。令(P,q)∈ reduct(<I 细因此R1sR2(l) R>)则由 reduct的构造得到(In]nlq]ln)∈R。于是据 综上可知,<,R1><H2,R2>。 <,R><E,7>可知,存在(A,B∈T使得[plnA 至此,已经证明了 reduct与 expand两个函数均具 引nsB从而根据 reduct的定义,(p,q)∈ reducto(<∑.有单调性,并且 reduct与 expand确实分别是PP到Re T> 以及Rel到PP的函数。下面将给出划分对与自反传递 下面给出函数 exp and的定义,该函数作川于一个的二元关系之间的相互关联。 元关系,并得到一个划分对。 引理4(伽罗瓦连接)若<Ⅱ,R>为G的划分对,≤ 定义6( expand函数)对于二元关系sPxP,为G下自反传递的二元关系,则rebc(<m,R>) expand(<)为定义如下的二元组<x7>,其中<表且仅当<,R> Expand(s) 示≤的目反传递闭包。 证明令 reduc(<,R>)=≤n段, expand(≤) E{{p≤qsp}p∈P} <∑,T>。 T{(A,B)P∈Aq∈B(P≤q)} (→)令p∈A∈。设p'∈A,故由≤n.s的构造 事实上,设p∈A,q∈B且p≤q。对于任意的 可知p=<nR>Ps≤n,R>P 已知≤n2三≤,故psp'≤ p'∈A,q∈B,有p'≤‘p且q≤q;进而基于≤'的传递P,从而由E的构造得到p'∈:故Ⅱ比E精细。 性可知p'≤'。因此,T同样可以通过如下等价方式类似可证R7(m)。因此<,R>E<E,7 构造 (←)令p≤n。从而,据≤n、的构造可知 7={(.B)vP∈Avq∈B(p≤q)} qn)∈Rc由于<,R> expand(≤),因此 下面的引理说明,利用cpmd得到的确实是划分[q]2)∈T。由定义5可知psq。因为≤具有自反传递 对,且该划分对是传递的 性,所以s=≤,即p≤q。从而sx,k≤ 引理2对任意二元关系 KcPxP,ep(≤)(=<∑ 引理5对于G的划分对<,R>以及G下自反传 7>)是划分对且7具有传递性 递的二元关系≤,有 证明首先,设A,B∈∑且A∩B≠⑧。因此,存在 (1)≤- reduct( expand(≤)。 r∈A∩B。设p∈A,q∈B,则由∑的构造可知p≤ (2)<1, R>-expand(reduct(<I, R>) r≤"p且q≤r≤q,于是据≤”的传递性得到p≤q且 证明(1)令 expand(≤)<Σ,T>。根据T的构造, q≤'p,因此A=B。故∑确实是划分。 P≤q当且仅当(pq-)∈T。同时由定义5可知 其次,由≤的自反性易知T仍具有自反性 ([]kg])∈T当且仪当(P,q)∈ reduct(<∑,T>)。 再次,设(A,B)∈7且(B,A∈7。令p∈A,q∈B, 2)令 reduc(<,R>)=≤n.2瓶 expand(≤<m.)= 则有p≤q且qs'p,因此A=B,无环性由此得证。从<m,R>。设P∈A∈且P∈'∈<I,R'>。则根据定 而<∑,T>确实是·个划分对 义6,对任意q∈P,q∈A当且仪当ps、mA、q≤n。 44 2016,52(17) Computer Engineering and Applications计算机工程与应用 由定义5与R的万环性得到psnR4≤mP当H仅p”∈P使得p→p"“p,从而由(Rs;)得到p"snq。 当q∈A。故=Ⅱ。类似可证R=R′。故<,R>= 因为p”,q稳定,故由(RS可知存在q∈Q使得q→|g <I,R'>。 且p'≤aq LLTS预备模拟的等价描述 (p,g→)出于p稳定,因此p→p"当且仅当 以定义3所给的方式定义预备模拟关系对于判定 =p”,则通过(RSi)可知存在稳定的q"∈Q使得 算法的实现有着如下的不是:其中对于稳定状态间和不q→q"且p≤a"。于是山(RSi)可知存在q’∈Q使得 稳定状态间是否具有预备模拟关系的判定条件有着较"s且p'≤q。同时结合g→"与q"=g得到 为明显的不同,若以该定义为出发点进行判定,则在稳 定状态间的预备模拟关系确定之前无法对不稳定状态 q→q 做出判断因而预备模拟关系的判定不仅要对状态进行 (p→,q→)同样可知存在稳定的p∈P使得 排序,还需要处理由状态是否具有稳定性所带来的不同p=”=’,于是由(RS得到存在稳定的q"∈Q使得 情形。为解决以上间题,本章将给出LS预备模拟关="且p≤"。对于pq",山(Rsi)可知存在 系的等价描述——泛化预备模拟关系,这一描述从一般 化的角度看待预备模拟关系,统一了稳定与不稳定状态 ∈Q使得q"→′且p'≤q。并由q→"与q"→g 间是否具有预备模拟关系的判定条件。之后将计明泛可知q→q′ 化预备模拟与LLTS预备模拟之间确实具有等价性,并 (GRS3)设p∈Fp且(p)∈I5(p)。则可知p→p, 提出与泛化预备模拟关系相对应的划分对稳定性的概 念,最终证明稳定划分对与泛化预备模拟关系等价 故山(R$得到存在q∈Q使得q→q′且p'≤anq'。因 首先,对于IITS中的进程P,给出其“稳定预备 此出pq'稳定及(RSiv)知I(p)=(q),即p)∈l 集”的概念。 (≤ω同样只需证明当p<q时<p,q>满足定 定义7(稳定预备集)令<P,→,F>为个LLTS 义3屮(RSi)、(RSⅱi)以及(RSi)。下面依次证明 进程P∈P的稳定预备集J(p)定义如下: (RSi)平凡成立。 5(p)={(q)→|9 (RSi)设p,q稳定且p→’。则由(GRS2)可知, 借助丁这一概念,给出LLTS预备模拟的等价描述存在q′∈Q使得q→l′且<p',q>∈R 如下。 (RSiv)设p,q稳定且pgFp。则由(LTS2)可知p 定义8Ls预备模拟的等价描述)令<P,→P可稳定因此l(p)≠②,故令1(P)∈1(P)。则有p→p F>以及<Q,),F>为两个Ts,RPxQ。若由于p稳定,故p=p,即ls(P)={1(p)}。由(GRS3)得 对丁任意<p,>∈R以及a∈A,下列条件均成立,则R到q≠F,且同样可知q)={(q)}。从而由1(p)≤ 是一个泛化预备模拟关系 3(q)得到I(p)=/(q) (GRS1)如果p→p',那么存在q∈Q使得q→q 令G=P.→>,F>为一个LLTS,A,B为P的任意 且<p,q'>∈R。 两个子集且a∈A,定义转换关系→为:A→B当且 (GRS2)如果p→p,那么存在q'∈g使得g=仅当存在p∈A,q∈B使得p=。并定义转换关系 且<p'.q'>∈ 为:AB当且仅当对于任意的p∈A,存在qEB (GRS3)如果p≠F,那么l(D)<l(q)。 若存在泛化预备模拟关系R使得<p,y>∈R,则使得P→ 记作p<q。 下面,将引入本文最重要的概念,即个划分对关 性质2≤=<。 于转换关系以及协调性谓词的稳定性。 定义9(稳定性)令G二<P,→,F>为·个有限 证明(≤a)只需证明当psa时<p,9>满TsG的一个划分对<,R>关于转换关系→与协 足定义8中GRS1).(GRS2)以及(GRS3)即可。下面依调性谓词厂稳定,当且仅当: 次讨论。 (GRS1)由(RS)可知<P,q>满足(GRS1)。 (1)对于仁意的A,B,C∈,若(A,B∈R且A→C (GRS2)从p,q的稳定性出发,分情形讨论 则存在D∈使得C,D)∈R且B→D,其中a∈A (P→,q分)由(RS)可知<p,q>满足(GRS2) 2)对于任意的A,B,C∈,若(4,B)∈R且A=C, (p→,q)由于p→p′,因此可知存在稳定的则存在D∈m使得C,D)∈R且B=D。 朱文涛:逻辑ITS预备模拟关系的判定算法 2016,52(17) 45 (3)若P∈F,则sF 证明(→)只需证明当<1,R>具有稳定性时 (4)对丁任意的A,B∈Ⅱ,如果(4,B)∈R且AF,rec(<1,R>)满足定义8中条件(GRS1)、(GRS2)、 那么对于任意的P∈A,g∈B,l5(p)sls(q)。 (GRS3)即可。设(4,B)∈R且p∈A,q∈B,则由 此时称<,R>为一个稳定划分对。对 J. LLTSG reduct(<1,R>)的构造可知(p,9)∈ reduc(<l,R>) 的任意划分对<Σ,T>,若满足<,R><Σ,>,则称 (GRS1)设p→m′。由此得到[]→[n。进而由 <I,R>是<E,T>的稳定精化。如果对于<∑,T>的 任意稳定精化<,R>均有<1,R><I,R>,则将<n.,R>稳定且(p]q)∈R,根据定义9(2)可知存在 <,R>称为<Σ,T>的最大稳定精化 D∈l使得(lD)∈R且ly→D,从而存在q'∈D使 例1LTSG1=<P1→,F>如图所示,其中F=得q→。同时由(pD)∈R可知(p,q)∈ reduct(<m s};图2与图3分别是G的一个划分对<x1,71>以及R>):所以,(GRS1)得证。 该划分对的一个稳定精化<S1>,其中T1=(E)是 GRS2)与(GRS1)类似 1上的自反关系,<1={(P1D1D)(PD3Dl1v1) (GRS3)设p与q稳定且pgFc则据定义9(3)可 ([gJg3])([s4[s)}∪r(s)。 知A¢F,从而由定义9(4)可知l3(m)ls(q)。枚 (GRS3)得证。 (∈)设ree(<H,R>)为G上的一个LITS预备 模拟,则只需证明<I,R>满足定义9中条件(1)~(4) 即可。 (1)设(A,B)∈R且A→C,则在p∈A,p'∈C 使得p→p′。令q∈B,则由(p,q)∈ reduct(<1,R>) 及(GRS2)可知,存在q使得q→g'且(p,q)∈ reduct(<1, 图1一个逻辑ITSG1=<P1,→1F1 R>),故B→[q]且Cq]∈R。于是令△{(E,F)∈ RB→E,B=F},山B→lq且R具有自反性可知 P p2 P3 P5 ([q]q]∈4,进而据R是有限集合上的偏序可知△仍 是有限偏序,故令D为中的极大元。出(CJqT∈R q 95 且(g小D)∈R得到(C,D)∈R;另一方面,由B→D得 到存在r∈B,r'∈D使得r→。令s∈B,则可知(,s)∈ reduct(<H,R>)。由于r→r’,据(GRS2)叮知,存在s S, S, S, SsS 使得s→s且(',s)∈ reduc(<Ⅱ,R>)。从而可知(D 图2G1的一个划分对<ET1> [勹)∈R;而此时必然有[s-D。故对于任意s=B,均 有s'∈D使得s=|',即B=D。故(1)得证 P (2)对于A→C,证明方法与(1)类似 (3)反设p∈F且存在q∈[以使得q丝F。由于 g3 ∈l,因此(q,p)∈ reduc(<l,R>)。由丁qF,据 (LTS2)可知q可稳定,即存在q'gF满足q→q’。因为 S, S, S, S, S F rect(<1,R>)是LLTS预备模拟且(q,p)∈ reduct(< 图3<21,1>的个稳定精化<S,<1> R>),根据q→q′及(GRS1)可知,存在p'丝F使得 下面的性质说明,G的一个传递的划分对<m,R>P→′。进而由→|的定义得到pgF,产生矛盾。因 具有稳定性当且仅当rehe(<m,R>)是G上的一个泛此不存在q[使得qF。 化预各模拟关系。 (4)设(A,B)∈R且A¢F。令p∈A,q∈B,则由 性质3令<,R>为有限 LLTS G的一个传递的划 reduct(<1,R>)的构造可知(p,q)∈ reduct(<,R>) 分对,则<m,R>具有稳定性当且仅当 reduct(<,R>)故由(GiRS3)可知(p)≤ls(q) 是G上的一个泛化预备模拟关系。 结合性质2、3以及引理1~5,有如下两条引理。 462016,52(17) Computer Engineering and Applications计算机工程与应用 引理6令<Σ,T>为有限 LLTS G的传递的划分 (3)对丁任意的p∈P,若p∈F,则n=p2∩F 对,则<Σ,T>始终存在唯·个最大稳定精化。 (4)对于任意的(A,B)∈R,如果A¢F,那么对于 引理7令G=<P,→,F>为一个有限IITS 任意的p∈A,q∈B,l(p)≤ls() ≤cPxP为P上自反传递的二元关系。则包含于≤的 (5)<I,R>二<∑,T'>。 最大LLTS预备模拟<与 expand(≤)的最大稳定精化 (6)对任意关于<∑.T>满足条件(1)~(5)的划分对 等价。 <,R'>均有<f’,R'>「<H,R>。 证明易知472 reduct(<2,T>),于是根据引 5判定算法 理3可知<,Rx<E,T>,从而<,R>[<∑,T> 通过以上工作,已经建立起LLS预备模拟与泛化<,R>关于<Σ,T”>满足条件(5)。由引理2可知R 预备模拟以姣泛化预备模拟与稳定划分对之间的等价,具有自反传递性。容易验证,<,R>关于<x′,'>满 从而使得判定不同LTS间是否仔在LLTS预备模拟的足条件(1)-(4),其证明与引理2类似。 问题可以通过求解最大稳定精化的方式进行解决。本 设<m,R>为G的任意个关于<2,7>满足条 章将借鉴 van glabbeek r j等人给出的判定通常模拟件(1)-(5)的划分对。设p∈∈m'。令p'∈A,则 关系的算子p",并对该算子的定义进行恰当的修改,(p,p)与(p,p均满足定义10中的构造条件, 以使该算子能够正确处理进程的协调性及稳定预备集,从而 pa.t>pas.r.p。据定义6可知p1,因 从而能够利用该算子获得本文中提到的划分对的最大此Asln。所以,比精细。 稳定精化”—具体而言,该算子对初始划分对进行精 化,以得到一个“更加稳定”的划分对,通过迭代,最终在 令q∈B'∈I且(,B)∈R,则同样可知pxr2q, 不动点处得到初始划分对的最大稳定精化 从而([p]nqn)∈R。由于m比Ⅱ精细,因此R'cR(I) 定义10(p算子)令G=<P,→,F>为一个有限 综上可知<′,R<,R>。即<I,R>关于 LTS,<E,7>为G的一个传递的划分对(即关系T需<2,7’>满足条件(6) 满足传递性)。定义p(<E,T>) expand(<x,7),其中 性质5(p算子的单调性)p算子关于匚单调,即, 小7PXP定义如下。 如果<∑,T>与<∑,T>是有限 LLTS G的两个传递的 划分对,且<Σ,7><∑,T>,那么p(<∑,T>)m(<∑', pxrq当且仗当p,q满足如下条件 (1)存在(A,B)∈T使得p∈A,q∈B 证明易知p<Σ,T>)关于<∑,T>满足性质4中 (2)若p≠F,则15(p)sl5(q)。 条件(1)~(5)。由于p(<∑',T>)关于<E′,T'>满足性 (3)对于任意的C∈2,若p,q稳定且存在P∈C质4中条件(1)-(5)以及(6),故p(<E,>)E(<x, 使得p→p',则存在D∈∑以及q’∈D使得C,D)∈TT>)。 且q→q 由丁p(<∑,T>)< 而匚是有限集上的偏 (4)对于任意的C∈∑,若存在p∈C使得p→p 序,因此可知,对<2,T>迭代应用p算子将最终达到不 动点,即是以下性质。 则存在D∈∑以及q'∈D使得(C,D)∈T且q→|g。 性质6(不动点)对于有限 LLTS O的一个传递的 从引理2可知,p(<Σ,T>)确实是一个划分对。下 划分对<∑,T>,存在n≥0使得 面将给出该划分对所具有的一些性质,这些性质将用于 p(<∑,7>)=p"(<∑,T> 说明p算子在不动点处具有稳定性。 引理8(不动点的稳定性)对于有限 LLTS G= 性质4令G=<P 为一个有限IITS P 的个传递的划分对<Σ,T>,p(<E,>) 2T>,<2,T">为G的两个传递的划分对且满足<x,r>当且仅当<,T>关于→与F稳定。 <∑,T[<∑,T>。令p(<∑,T>)=<m,R>,则<,R> 证明(→)p(<Σ,T>)-<∑,T>时<2,T>关于自 关于<∑',T'>满足如下条件 身满足性质4中条件(1)~(4),即<∑,T>满足稳定性 (1)对任意的A,B∈以及任意的C∈E,若(见定义9)。 (A,B)∈R且A→C,则存在D∈∑使得C.D)∈T"且 (←)只需证明<Σ,T>稳定时关于自身满足性质 B→{sD,其中a∈A: 屮条件(1)~(6)即可。 (2)对任意的A,B∈Ⅳ以及任意的C∈∑′,若 <∑.7<E,T>平凡成立。当<∑,T>稳定时其 关于自身满足性质4中条件(1)~(4)。设<Ⅰ,R>为任 (4,B)∈R且A=C,则存在D∈E使得CD)∈T且意关于<E7>满足(1)-(5)的划分对,则必然有 B→|D .R>匚<Σ,T>:因此<Σ,T>关于自身满足性质4中 朱文涛:逻辑ITS预备模拟关系的判定算法 2016,52(17) 4 条件(6) Sw1 S2 结合性质5以及引理8可知,对于·个传递的划分 (SWI SW2-1 对<∑,7>,p算子将通过一个由划分对构成的单调序 列向<∑,T>的最大稳定精化不断靠近,即是以下引理。 引理9令<Σ,T>与<I,R>为有限 LLTS G的两 个划分对,且R具有传递性。令<S,~为<∑,T>的最 sW1-2 SW2-2 大稳定精化。若<S,<1,R>,则<S,<以(<I, R>) 证明由于<S,心是稳定划分对,且由引理2可知 具有传递性,故由引理8知p(<S,∞)=<S,<>。设 AS-1 <S,∞>「<H,R>。因为<与R具有传递性,所以由性 质5可以得到p(<S,→)匚p(<1,R>),即<S,<>匚 p(<H.R>) oF-2 通过以上的性质与引理可知,当对G的划分对 ( Con-3 <∑,T>反复应用p算子直至到达不动点时,可以得到 <∑,T>的最大稳定精化,即是下面的定理。 图4抽象规范Spec 定理1令<5,T>为有限 LLTS G=<P,),F>的组成的简单开关:上部的初始状态—关闭状态SW1-1 个划分对,令<S,为G与<∑,7>构成的GCPP的(SW2-1,以及下部的开启状态SW1-2(SW2-2):通过动 解。设n为使得p(<∑,7+>)=p(<2,m>)成立的作sw1(sm2)可以在两个状态之间切换,同时可以通过 最小自然数,则p"(<∑,T>)=<S,< 自环an1(on2)表明开关已被开启。 证明山性质6可知n确实存在。只需分别证明 组件AS川以描述系统的调度:任意时刻sw1与 p(<E,7>)<S,与<S,EP"(<∑,T>)即可 5v2功作至少有一个可以执行;在此处以¨“sw1,sw2”代 (n(<E,7+>)<S,)由性质4(5)可知(<∑,表了两个转换:一个swl转换以及一个sw2转换。直观 T>)<∑,7>,并且由引理8可知,p(<,T>)关于上,AS可以看作时序逻辑公式“ always(swl v sw2v 〉与F稳定。根据最人稳定精化的定义,对于( (swash2)”,其中口表示外部选择 <ΣT>的任意稳定精化<Ⅱ,R>,均有<,R>匚 逻辑 LTS Con则表示系统的限制:任意时刻两个模 <S,>,因此p(<∑,T+>)<S,∞>。 式不能同时处于开启状态。该LTS由一个初始状态 v、(:,E(<2,>)根据最大稳定精化的定义,Com-1与一系列x-分支构成,每个分支的预备集是 ><E,T>:对此应用n遍引理8,则得到<S.{on1,on2,sw1,sw2}的子集,互不相同,并且on1与on2 ☆>p"(<E,T+> 不同时在一个预备集中出现。简洁起见,图中仅表现了 A、A、A"三个分支而省略了其他。每个τ-分支可以 6实际例」 通过其动作集中的任一动作返回到初始状态,同样,为 本章给出一个小型的实际例子,用以说明LLTS精 保持简洁,这些转换在图中统一由标记为该分支动作集 化关系的实际应用。该例子通过逻辑LIS的形式给出 的转换代替:约束Con可看作是由时序逻辑公式 always(On1∧On2)”所产生的。 了交通信号灯控制系统屮红绿灯的控制模式逻辑的规 范以及实现(此处的“模式”即对应于并发理论中的状 通过文献7可知,上述规范状态繁多,转换关系复 态)之后借助给出的p算子验证规范与实现之间存在杂,在设计过程屮很难进行实际应用,因此需对其进行 凊化关系,从而保证实现的正确性 精化以得到一个可操作的实现。逻辑 LTS Impl给出了 Spec的具体实现如下: 例2对于该模式逻辑的简要描述如下:该模式逻辑 由两个模式开关组成,其中每个开关控制一个模式是否 Impl=(sw, Sw,lICC,) 开启,同时系统的调度要求任意时刻至少有一个开关能 由逻辑LTS中‖操作符的结合性及交换性可知, 够执行开关动作,并旦限制仟意时刻只有一个模式能处该实现等价于(SW|S2米cCC2),因此只需验证 于开启状态。 CCCC2≤然AS并且(SWSW2米CC1CC2≤COn,即 由上述要求,给出该模式逻辑的规范如下 可由定理16得到(SW1|SW2米NCC1CC2)≤ RS Spec SpeC=(SW1|SW2|AS)∧C 为验证 CCCC2≤AS,首先给出CCCC2与A5 其中逻辑 LTS SP1(S类似)描述了一个由两个状态构成的逻辑[TS如下 482016,52(17) Computer Engineering and Applications计算机工程与应用 R及van( Glabbeek R.J等人给出的判定通常模拟关系 CC1-1 的方法,本文给出了用以求得最大稳定精化的算子p 并证明了其正确性,从而得到给定的LLTS上最大的预 sw2 swl 备模拟 至此,已经完成了求解LLTS预备模拟的工作。接 下来,将尝试寻找是否存在更加高效的对该问题进行求 CC1-2 CC2-2 解的算法。 \Swl CCI SW2 CC2 SC1-1 SC1-2 SC2-1 XC2:2)参考文献 [1] Bergstra J A, Ponse A, Smolka S A Handbook of pro- 2 cess algebra[M]-[SL]: Elsevier, 2001 [21 Baeten J C. M, Basten T, Basten T, et al. P equational theories of communicating processesM-ISI.: SC1-3 SCI-4 SC2-3 sC2-4 Cambridge University Press, 2010 process algebra].TE 图5具体实现lmpl retical Computer Science, 2005, 335(2): 131-146 1 Blackburn P, Van Benthem J, Wolter F. Handbook of modal logic[M]S 1.1: Elsevier, 200 5 Merz sOn the logic of TLA+[J Computing and Infor- matics 2012 [6] Luttgen G. Vogler W Conjunction on processes full abstrac 2 sw l sw2 tion via ready-tree semantics[J]. Theoretical Computer Sci cnce,2007,373(1):19-40 [7] Luttgen G, Vogler WReady simulation for concurrency it's logical! [JInformation and Computation, 2010, 208 图6CCCC2与AS构成的逻辑LTS (7):845-867 将上述逻辑ITS看作划分对<∑7>,其中∑=[8] Lutlgen G, Vogler W safe reasoning with logic1s {P},P={p,q,r,S,u,v,w,2},T=∑x∑。对其应用p Theoretical Computer Science, 2011, 412(28): 3337-3357 算子,首先得到划分对<E,71>,其中1={P11 [9] Berard B. Bidoit M, Finkel A, et al. Systems and sofi ware verification: model-checking techniques and tools[M] 7,l3,P1={,q,,s,w,V=v},71={2},U1={u4}, LS.l」: Springer,2010 T1=(UDV,C(2,UU(E)。对<,7>再次使101△ bulla p a., Legay A,d'OsoJ, et al.Tree regular 用p算子将得到划分对<2,2>,E2={P2,V2,Z2,U2W2 model checking: a simulation-based appruachJ]The Jour P2={P,q,,s},H2={ν,22={2},U2={,W2={w}, nal of Logic and Algebraic Programming, 2006, 69(1) T2={(P2,C2)W2,U2)2,U2)(Z2,U2)(P2,W2)}(E2) 93-121 对<∑2,T2>使用p算子将得到该划分对本身,因Gani, Piazza C, Policriti A from bisimulation to simulation: coarsest partition problems]Journal of Aut 此<∑2,72>即为最粗划分,可以看到p≤,是 Imated Reasoning, 2003, 31(1): 73-103 CC|CC2≤gsAS。对于(SW1SW2)CC|CC2)≤B5COn,[12] Van glabbeek R, Ploeger B Correcting a space- fficient 验证过程类似。从而,利用p算子,验证了实现mpl是 mulation algorithm[C]Computer Aided Verification 规范Spec的精化 Berlin/ Heidelberg Springer, 2008: 517-529 [13 Rafa S, Ranzato F, Tapparo F Saving space in a time 7结束语 efficient simulation algorithm [J]. Fundamenta Informati- cae,2011,108(1):23-42 本文回顾了逻辑标记转换系统以及其上的预备模 [14 Ranzalo FAn efficient simulation algorithm on Kripke 拟关系;提出了与LLTS预备模拟关系等价的泛化预备 structures[J]. Acta Informatica, 2014, 51(2): 107-125 模拟关系概念以及与泛化预备模拟等价的稳定划分对15] Markovski I Saving time in a space-efficient simula 的定义;并着重探讨了泛化预备模拟与稳定划分对之间 tion algorithm[C]/International Conference on Quality 的紧密联系,借助于二者之问的等价性,并参考 Gentilis Software,2011:244-251

...展开详情
试读 8P 论文研究-逻辑LTS预备模拟关系的判定算法.pdf
立即下载 低至0.43元/次 身份认证VIP会员低至7折
    抢沙发
    一个资源只可评论一次,评论内容不能少于5个字
    weixin_38744153 你的留言是对我莫大的支持
    2019-09-11
    • 至尊王者

      成功上传501个资源即可获取
    关注 私信 TA的资源
    上传资源赚积分,得勋章
    最新推荐
    论文研究-逻辑LTS预备模拟关系的判定算法.pdf 6积分/C币 立即下载
    1/8
    论文研究-逻辑LTS预备模拟关系的判定算法.pdf第1页
    论文研究-逻辑LTS预备模拟关系的判定算法.pdf第2页
    论文研究-逻辑LTS预备模拟关系的判定算法.pdf第3页

    试读已结束,剩余5页未读...

    6积分/C币 立即下载 >