没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记99(2004)127-154www.elsevier.com/locate/entcs信息流安全中的放松*A. 博西河Focardi2 D. Macedonio3 C. 广场4南罗西5DipartimenntodiInforormatica,Universit`aCa摘要我们研究信息流的安全属性是持久的,在这个意义上说,如果一个系统是安全的,那么它的所有可达状态也是安全我们提出了一个统一的表征这些属性的一般展开模式。这种展开的表征使我们能够证明所考虑的安全类的几个组合属性。此外,我们利用解卷条件来决定我们可以使用的规则的形式,以逐步开发安全的过程,并纠正不安全的过程。1介绍信息流安全属性已被提出作为确保多级系统中分类信息这些属性对具有不同安全级别的不同实体组之间的信息流动施加约束通常只考虑两个组,并标记为高(H)和低(L)安全级别。条件是没有信息从H流到L。*本工作由MIUR项目“Mo delli formalipe r la- curezza”、欧盟项目MyThS(IST-2001-32617)和FIRB项目(RBAU 018 RCZ)“I n t err p et a zi o ne a st r a tta e mo del cheching p e rla v e rifica di system i em i e edded“提供支持。1 电子邮件地址:bossi@dsi.unive.it2 电子邮件地址:focardi@dsi.unive.it3电子邮件:mace@dsi.unive.it4电子邮件:piazza@dsi.unive.it5 电子邮件地址:srossi@dsi.unive.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2004.02.006128A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154控制信息流作为一个整体(直接和间接)的必要性促使Goguen和Meseguer引入了不干涉的概念[19,20]。非干扰形式化了确定性系统中信息流的缺失。在一个系统中,机密(即,高级)和公共(即,低电平)信息可以共存,非干扰要求机密输入永远不会干扰系统公共接口上的输出,即,永远不要干涉低级别用户。如果这样的性质成立,人们可以得出结论,从高到低水平的信息流是不可能的。从Sutherland [36]开始,文献中提出了许多将非干扰概念扩展到非确定性系统的定义它们是在不同的环境中开发的,如编程语言[4,33,34,35],跟踪模型[25,26],过程演算[11,14,22,30,31,32],proba,bilistic模型[2,12],定时模型[15,21],加密协议[1,5,16]。在[13]中,Focardi和Gorrieri表达了不干涉的概念,安全进程代数(SPA)语言,在互模拟语义方面特 别 是 , 受 [37] 的 启 发 , 他 们 引 入 了 基 于 互 模 拟 的 非 演 绎 组 合(BNDC)的概念:如果低级别用户看到的系统没有通过与E组合任何高级别进程来修改(在互模拟语义的意义上),则系统E是BNDC。BNDC相对于基于跟踪的属性的主要优点是,它足够强大,可以检测到由于高级别恶意进程阻止或解除阻止系统的可能性而导致的信息泄漏。特别地,在[13,14]中,显示恶意进程可以通过适当地阻止和解除阻止低级别用户可访问的某些系统服务来建立从高到低的通道。用于构建这种隐蔽通道的系统在基于痕迹的属性方面是安全的。这促使使用更有区别的等价物,如互模拟。虽然Martinelli [24]已经证明了一类BNDC性质在有限状态过程上是可判定的,但有效地验证BNDC的问题仍然是开放的。事实上,BNDC的可判定性是一个开放的问题。主要的困难在于摆脱对高级过程的普遍量化。BNDC的另一个缺点是,它与主要的SPA操作符(如并行组合和不确定性选择)不兼容。组合性结果是有用的,因为它们有助于设计有效的验证算法和定义证明系统,允许人们逐步构建通过构造而安全的系统。由于这些原因,文献中已经研究了BNDC的许多可判定的和合成的充分条件。 在[9]中,已经证明了这些充分条件中的四个,即持久BNDC(P BNDC),A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154129强BNDC(SBNDC)、组成P BNDC(CP BNDC)和进展P BNDC(PPBNDC)可以根据解旋条件来表征。放松条件要求个体动作的属性:它们旨在正如许多作者所观察到的那样(见[31,29,23,32]),它们更容易处理,并且更适合于全局条件下的自动证明在本文中,我们弥合了解旋条件和组合性之间的差距。特别地,我们引入了一个参数化的解旋概念,它推广了[9]中考虑的解旋特征。我们利用参数解旋条件给出了一般的合成结果. 这样的结果旨在建立语义之间的联系我们希望确保组合性的操作符和展开条件中涉及的关系。PBNDC、SBNDC、CP BNDC和PP BNDC的合成性质只是我们的一般结果的本着同样的精神,我们分析了如何在精化下保持解旋条件(见[8])。通过利用参数展开条件及其一般组合性质,我们还可以定义证明系统(见[7]),使我们能够构建通过构造而安全的过程。最后,我们提出了纠正(见[6])不安全进程的方法,以获得满足表征特定安全属性的展开条件的进程。本文件的结构如下。在第2节中,我们回顾了SPA语言的语法和语义。在第3节中,我们介绍了安全性质BNDC和P BNDC。此外,在第3.1节中,我们定义了一个通用的展开模式,并给出了安全属性P BNDC,SBNDC,CP BNDC和PP BNDC作为通用模式的不同实例的统一表示。在第4节中,我们分析了关于SPA算子和细化的解卷条件和组合性之间的关系。我们利用这些结果开发证明系统,其特征在于通过解旋。在第5节中,我们利用一般的展开模式提出了一种纠正不安全进程的方法。最后,在第6节中,我们得出了一些结论。本文综述了作者以前的工作[6,7,8,9,10]。上述的一般框架是一个原始的贡献,使我们能够统一提出我们的结果,也推广其中的一些130A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-1542预赛在本节中,我们将报告我们所考虑的进程代数的语法和语义。它是Milner的CCS [ 27 ]的变体除了常量定义之外,我们还允许使用复制(!)用于定义递归系统的运算符。我们的进程代数的语法基于与CCS相同的元素,即:一组可见动作L,使得L=I=O,其中I={a,b,. . }是一组输入项,O={a<$,<$b, . . . }是输出操作的集合;模拟内部计算的特殊动作τ,即, 在系统外不可见;一个补函数<$·:L→L,such thata<$=a,对所有a∈ L。 Act = L <${τ}是所有动作的集合。 可见操作集为分为两组,H和L的高和低的行动,使H=H所以L=L。SPA术语6(或过程)的语法定义如下:E::= 0 |a.E |E + E |E|E |E\v |E [f] |Z|!E当rea∈Act ,v<$L,f:Act→Act满足f(α<$) =f(α),f(τ) =τ,f(H)<$H<${τ},f(L)<$L <${τ},Z是一个常数,必须是一个有定义的常数,其中Zd=efE.直观地说,0是什么也不做的空进程; a.E是一个可以执行动作a,然后表现为E的进程; E1+ E2表示两个进程E1和E2之间的非确定性选择;E1|E2是E1和E2的并行组合,其中执行是交错的,在互补的输入/输出动作上同步,产生内部动作τ;E\v是被阻止在v中执行动作的进程E;E[f]是其动作通过重新标记函数f重命名的进程E;!E(bang E)是过程E|E|......你好。. ,即,与过程E所需的一样多的副本的并行合成。我们说,一个进程E是被保护的,如果它可以通过使用规则来构建a.E+a.E,而不是上述SPA术语语法中的E+E我们用E表示所有SPA进程的集合,用EH表示所有高级进程的集合,即,只使用H <${ τ }中的动作构造的那些。SPA代理的操作语义是根据标记转换系统(LTS,简称)。A LTS是一个三元组(S,A,→),其中S是一个6实际上,SPA语法不包括!操作符. 我们保持我们的语言的名称SPA,因为添加!并没有增加语言的表达能力。A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154131需要至少一个状态集,A是一组标签(动作),→S×A×S是一组标记过渡。记法(S,a, S)∈→(或等价于S→aS)means1 2 1 2系统可以通过动作从状态S1移动到状态S2a. SPA的操作语义是LTS(E,Act,→),其中状态是代数的项,转移关系→ E → E ×Act×E是由结构归纳法定义为图1中描述的推理规则生成的最小关系。我们还使用的概念,根标记的过渡系统,这是一个LTS增加了一个区别节点,根。 给予我们用LT S(E)=(SE,E,Act,→)表示过程E,根LTS构成从E可达的SPA LTS的子部分。 E是一个有限状态过程如果有一个有限的节点,那么SE是有限的。观察等价的概念是用来建立平等的进程之间,它是基于这样的想法,即两个系统具有相同的语义,当且仅当它们不能区分由外部观察者。这是通过定义E上的等价关系得到。 强互模拟关系[27]等同于两个过程,如果它们能够相互模拟它们的一步一步的行为。我们将使用以下辅助符号。Act表示动作序列的集合(可能为空),而Act+表示非空的a1an行动的顺序如果t=a1···an∈Actn且E→···→EJ,则我们写E→tEJ。如果E(→τ)n→a1(→τ)n· ··(→ τ)n→an (→τ)n∈EJ,则E=a1(→τ)n∈EJ,其中(→τ)π表示τ标记跃迁的(可能的)等时跃迁。 如果t∈Act,则nt∈L是通过从t中删除τ的所有发生s而需要的序列。As一个结果,E=aEJ代表E=a如果a∈L,则EJ,如果a=τ(注意,τ标记的过渡,而=表示零个或多个标记为τ的跃迁)。 我们说,EJ可达自当存在e时,t∈Act,则t为E→t从E可达的所有状态的集合。EJ。 我们用Reach(E)表示强互模拟的概念可以通过模拟来定义预订如下。定义2.1[模拟]代理上的二元关系R E × E是模拟如果(E,F)∈ R意味着,对于所有a∈Act,• 如果E→aEJ,它存在于FJ中,因此F→aFJ和(EJ,FJ)∈ R.一个主体E被另一个主体F模拟,记为E≤F,如果存在一个包含对(E,F)的模拟R关系≤是最大的模拟,它是一个前序关系,即, 它是自洽和传递性。τ132A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154EEE12一2一1211Prefix总和E→a−a. E→aJ1EE →aJE1+E2→JE1+E2→JE1→E|E→aJ1EJ|EE2→E|E→aJ2E|EJ平行1 21E→a2JE21→a<$2 12J2a∈ LE|E→τ EJ|EJ1 2 1 2限制E→aE\v→aEJEJ\v如果a/∈v重新贴标E→aEJf(a)E[f]→EJ[f]恒定复制E→aE→aZ→aEJEJEJE→a如果Zd=efEEJE→a<$EJJa∈ L!E→ EJ|!E!E→EJ|EJJ|!EFig. 1. SPA的操作规则定义2.2[强互模拟]主体上的二元关系R E ×E是强互模拟,如果R和R−1都是模拟。两个智能体E,F∈ E是强互相似的,记为E<$BF,如果存在包含(E,F)对的强互模拟R关系B是最大的强互模拟,它是一个等价关系。在许多应用中,强互模拟要求太高,即,它太精细了。特别是,内部转换被视为所有其他动作。弱互模拟关系类似于强互模拟关系,但它不关心内部τ作用。EEEEEτ一一一A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154133BB⇒P⇒定义2.3[弱互模拟]主体上的二元关系R <$E ×E是弱互模拟,如果(E,F)∈ R蕴涵,对于所有a∈Act,• 如果E→a• 如果F→aEJ,则FJ存在,满足F=aFJ,如果EJ存在,则E=aFJ和(EJ,FJ)∈R;EJ和(EJ,FJ)∈R.两个智能体E,F∈ E是弱双相似的,记为E<$BF,如果存在一个包含(E,F)对的弱互模拟R关系B是最大的弱互模拟,它是一个等价关系[27]。在我们的安全性质中,我们需要低动作上的弱互模拟的概念,这等同于从低级别用户的角度来看是互相似的过程,以及低动作上的进展互模拟,这也要求每个τ动作至少被一个τ模拟。定义2.4[弱互模拟低动作]二元关系R <$E× E是一个弱互模拟低动作,如果(E,F)∈ R意味着,对于所有l∈L<${τ},• 如果E→1• 如果F→1则存在FJ使得F FJ,则存在EJ使得E=lFJ和(EJ,FJ)∈R;=lEJ和(EJ,FJ)∈ R.两个智能体E,F∈ E在低作用上弱双相似,记为El F、如果存在包含对(E,F)的弱互模拟R可以立即证明, F等价于E\H<$BF\F。在低动作上进行互模拟类似于在低动作上弱互模拟。动作,但它是基于[28]中引入的渐进互模拟的概念。定义2.5[低动作上的渐进互模拟]主体上的二元关系R <$E ×E是低动作上的渐进互模拟,如果(E,F)∈R意味着,对于所有l∈L<${τ},• 如果E→1EJ,则FJ存在,使得F=FJ和(EJ,FJ)∈R;• 如果F→1FJ,如果EJ存在,则E=1EJ和(EJ,FJ)∈ R.两个智能体E、F在低动作上进行双向相似,用E表示 F、如果存在包含对(E,F)的弱互模拟RL134A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154Bh hh图二. 存储器单元M x的LTS。3基于互模拟的安全性质在[13]中,Focardi和Gorrieri通过基于互模拟的合成非演绎性(BNDC)的概念,用互模拟语义表达了非干扰的概念属性BNDC基于检查系统是否存在所有高级潜在交互的想法,代表每一个可能的高级恶意程序。特别地,系统E是BNDC,如果每一个高级进程都是一个低级用户无法区分E和(E|),也就是说,如果系统E不能干扰系统E的低层执行,在换句话说,一个系统E是BNDC,如果一个低层用户看到的系统没有通过组成任何高层进程来修改。定义3.1 [BNDC]设E∈ E. E∈BNDC,如果∀Π∈EH, E≈l(E)|)例3.2让我们考虑一个二元代数胞腔的抽象规范M x。Mx包含二进制值x,并且可由高和低用户通过分别表示高读、高写、低读和低写的四个操作rh、wh、rl、wl每一项操作都是通过两个不同的动作,每个动作对应一个二进制值。例如,wh0和wh1分别指示高级别用户写入值0和1。图2描述了进程M x的LTS。Mxd=efrx。 Mx+w0. M0 +w1。M1+r l x . M x+w l0。M 0+ w l1。M1请注意,读(写)操作被建模为输出(输入)。进程M x可以通过两个输出动作rh x和rl x发送存储值x。此外,通过接受输入wh y[7]下面M x的表达式实际上是一个定义方案:实际过程M0和M1是分别用0和1代替xA. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154135(1)(2)(3)(4)(5)(6)(7)(8)(9)(10)(1将y存储到存储器单元中。注意,M0和M1是完全不安全的进程.事实上,高级别用户可以使用存储单元直接向低级别发送机密信息。使用BNDC,我们检测到M0和M1是自信这里事实上,考虑到过程中的H1. 0我们得到(M0| M)\H <$τ.M1\H与M 0 \ H不是弱双相似的,因为在τ.M1\H中,低级别用户读取1,而在M0\H中,他读取0。在[14]中,Focardi和Gorrieri观察到BNDC性质在实践中很难使用:它的可判定性仍然是一个悬而未决的问题。它将最好有一种替代的BNDC公式,它避免了对高层次过程的普遍量化,只利用局部在寻找这样一个替代特征时的一个主要困难来自于BNDC不是持久的,因此对从BNDC进程E可到达的进程的需求应该不同于对E本身的需求在[17]中,引入了一种称为持久BNDC(简称P BNDC)的安全属性定义3.3 [P BNDC]设E ∈ E. E ∈ P BNDC如果EJ∈Reach(E), EJ∈ BNDC。P BNDC在有限状态过程上的可判定性已经在[17]中通过利用基于互模拟的表征得到了证明。保护机密数据的标准方法是应用[3]的多级安全模型首先,我们需要为任何信息容器(称为对象)分配一个安全级别;然后实施以下访问控制规则(i)没有低级别用户可以从高级别对象读取;(ii)没有高级别用户可以写入低级别对象。事实上,这是泄露机密信息的仅有的两种(直接)方式。有时它们足以确保安全性,如下例所述。示例3.4示例3.2的存储器单元既不是BNDC也不是P BNDC。为了保护机密数据,我们可以通过消除任何低电平读取操作(上面的规则(i)),M hxd=efrhx。 M hx+wh0。 M h0 +Wh1。M h1+w l0. M h0+ w l1。M h1和低电平单元M1 x,通过消除任何高电平写操作(上述规则(ii)):136A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154hl图三.存储器单元M hx的LTS。M lxd=efrx。 M lx+rx。M lx+w l0. M 10+ W 11。M l1我们可以证明Mhx和Mlx都是PBNDC.其他基于互模拟的持久安全属性已经在文献中进行了研究。我们在这里回顾以下内容:强BNDC(简称SBNDC),在[13]中介绍,组合PBNDC(简称CP BNDC),在[8]中介绍,和渐进P BNDC(简称PPBNDC),在[9]中介绍。所有这些属性都包含在BNDC类中,即,如果一个过程满足其中之一,那么它就是BNDC。在下一小节中,我们通过统一的展开定义来介绍它们。3.1展开定义展开概念背后的思想是在系统的转移上引入一些约束(参见[32]),这意味着一些全局性质。特别是,当使用展开条件来定义非干扰属性时,它通常要求每个高级别动作都可以以在本节中,我们通过引入广义展开条件,给出了安全性质P BNDC、SBNDC、CP BNDC和PP BNDC的统一表示。我们的解旋是关于过程的两个二元关系的参数:等价关系,~l,它表示低水平的不可逆性和过渡关系,−−·,它表征解旋条件所需的局部连通性。定义3.5[广义展开]设~l是E上的二元等价关系,−−·是E上的二元关系。我们定义解旋类A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154137BτˆBBPτBW(~l,−−·)作为W(~l,−−·)d=ef{E∈E|<$F,G∈Reach(E)andnd<$h∈H若F→hG,则n∈GJ满足hatF−−·GJ和G~1GJ}.一个解旋类的解旋状态特征显然意味着持久性。此外,任何不执行高水平的过程E都可以被称为过程E。动作属于任何解旋类W(~l,−−·),因为解旋的con-i-i-i这是一种平凡的满足。下面的定理来自于[7]中研究的P BNDC和[9 ]中研究的PPBNDC的解旋特征,以及[13]中SBNDC和[8]中CP BNDC定理3.6(解绕)设E∈ E是一个过程.• E∈P BNDC i <$E∈W(n,= n);• E∈SBNDC i <$E∈ W(n,n);• E∈CPBNDCi <$E∈W(τl,=τl);• E∈PP BNDC i <$E∈W(n,= n);其中,R2是进程之间的语法相等。上面的定理帮助我们理解我们的安全属性的局部含义设F是从P个BNDC过程E可达的过程. 如果F可以执行到达进程G的高级别转换,那么F也可以通过一个(可能为空的)静默过渡,一个过程GJ,它是从低层次上无法区分G风景在SBNDC的情况下,无声转换的序列被无转换替换,即,GJ是F本身,而在CP BNDC和PP BNDC的情况下,静默序列不能为空。此外,在PP BNDC弱互模拟低动作取代进展互模拟低动作。示例3.7考虑示例3.4中描述的存储器单元Mh x和Ml x。利用定理3.6中给出的PBNDC的解旋特征,很容易看出Mh0和Mh1都是PBNDC。第一、注意,Mh0等于Mh 1,因为低级别用户无法显示-在两个国家之间徘徊。 事实上,唯一可能的低级别动作是两个写操作wl0、wl 1,它们在Mh0和Mh1中都将系统移动到相同的状态。Ml0和Ml1是P BNDC的事实甚至更容易证明:仅有的高级动作rh0、rh 1不改变系统状态。 此外,由于Mh x和Ml x都不执行138A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154h hhhlBNDCP_BNDCSBNDCPP_BNDCCP_BNDC见图4。存储器单元N hx的LTS。图五.安全属性。任何τ跃迁,可以推断它们也是SBNDC。最后,可以注意到Mh x和Mlx既不是CP BNDC也不是PP BNDC,因为这两个过程不存在可执行的τ现在考虑通过在Mh x和Ml x的初始状态中添加由τ环实现的超时而获得的过程Nh x(参见图4)和Nl x,即,N hxd=efrx。 N hx+w0. N h0 +w1。N h1+w l0. N h0+ w l1。Nh1+ τ。N hxN lxd=efrx。 N lx+rx。N lx+w l0. N l0+ w l1。Nl1+ τ。Nl x.进程Nhx和Nlx都是CP BNDC和PP BNDC。解旋特征使我们能够很容易地证明PP BNDC的解旋性质。CP BNDC、SBNDC、BNDC和流程 含有只有低级别的动作才能满足所有这些要求。 有关情况概述于图5.A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-1541394如何逐步构建安全流程组合性对核查和综合都很有用。一方面,如果一个性质在系统组成时保持不变,那么分析过程可以分解并应用于子系统,以证明系统作为一个整体满足所需的性质。另一方面,在系统的合成中,组合性使得以统一的方式处理所有子组件成为可能。在本节中,我们分析了解卷条件与组合性结果之间的关系。我们证明了我们考虑的所有安全属性都是关于并行操作符的组合,而不是所有的都是完全组合的。特别是,P BNDC和SBNDC不保留的非确定性选择操作者。一般来说,当我们构建一个系统,它可以(非确定性地)选择作为两个安全子系统之一时,我们可以得到一个安全系统。正如[18]中所观察到的,这似乎是违反直觉的。相反,PP BNDC和CP BNDC是完全组成的,即,它们对于非确定性选择也是组合的。除了标准的代数运算符,我们还考虑了精化运算符,这对逐步开发安全过程很有用事实上,人们通常从所需系统的非常抽象的规范开始,然后对其进行细化和分解,直到达到可以直接实现的具体规范。如果性质在每个细化步骤下都得到保留,那么在某个阶段已经研究过的性质就不需要在以后的阶段重新研究给定一个解旋类W(l,−−·)和一个偏函数f:Ek −→ E,我们说W(l,−−·)关于f是合成的,如果E1,.,Ek∈ W(E1,−−·)意味着f(E1,.,Ek)∈ W(E1,−−·)或f(E1,.,Ek)不定义为d(表示为d byf(E1, . . ,Ek)↑).为了研究解旋类的组合性属性,我们首先引入以下保留和反射的概念。定义4.1【保持与关系】设f:Ek−→E是一个偏函数,且f ∈E × E是一个关系。函数f在下列条件成立时保持为f。 让本人J是任何{1, . . . ,k},其中。If<$i∈I(Gi<$GJ)andnd<$j∈J(Gj<$GJ)I j然后f(G1, . . ,Gk)f(GJ, . . . ,GJ)或r(f(G1, . . ,Gk)↑和f(GJ, . . ,GJ)↑)1k1k如果以下条件成立,则函数f表示f。 如果f(G1,.,G k)140A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154M,则I,J,I,J ={1,. ,k}且I/= k,使得i∈I(Gi<$GJ)andndi∈J(Gj<$GJ)andndM<$f(GJ, . . 、GJ)ij1k上述定义中的条件I/=I/的目的也是考虑非相关性关系,例如: 关系→h。例4.2设f是弱互模拟关系,即,当且仅当E<$BF。它认为并行复合算子保持弱互模拟[27]。另一方面,非确定性选择运算符不保持弱互模拟。事实上,0Bτ。0,但a。0+0/100Ba. 0+τ。0的情况。设可达性关系为,即,{(E,F)|E∈ E和F∈ Reach(E)}。并行运算符反映的 是。 事实上,如果G1|G2到达M,即,M∈范围(G1|G2)则M<$GJ|Gj,其中GJ∈Rach(G1)和GJ∈Rach(G2).1 2 1 2解旋类的组合性可以通过下面的定理来证明。定理4.3(反射保持复合)设f:Ek−→Ebeapartialfunctionalrect ing→h可达关系和保持-- 则W(l,−−·)相对于f是合成的。证据 假设k= 2不是限制性的。设E,F∈W(εl,−−·).我们必须证明f(E,F)∈W(l,−−·)。如果f(E,F)到达M,那么,由于f反映可达性关系δ,存在G,K(其中之一可能分别等于E或F),使得EF是K,M是G,M是K。如果M→h→h,这是可能的:那么,由于f• G→h• K→hGJ和MJ<$f(GJ,K);KJ和MJ<$f(G,KJ);• G→hGJ,K→hKj和M J<$f(GJ,KJ)。在第一种情况下,G−−·GJJ和GJJ<$lGJ。 因此,由于f保持−−·,我们有M−−·f(GJJ,K)和f(GJJ,K)<$lf(GJ,K)。第二种情况和第三种情况是相似的。因此,f(E,F)∈W(l,−−·)。Q正如我们将在下一小节中看到的,当我们处理其语义是递归的定义在子进程上(例如,并行运算符|). 其他运营商有8 注意,可达性关系是自反的。A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154141一QH作为子进程语义的“联合”的语义(例如,非确定性选择算子)。为了处理这类算子,我们引入了传播和投影的概念。定义4.4【传播与投影】设f:Ek−→E是一个偏函数,且f ∈E × E是一个关系。如果流动条件成立,则函数fp ro p ag成立。如果你是这样的话,(Gi<$GJ),nf(G1, . . . ,Gk)<$GJ或f(G1, . . ,Gk)↑.我我如果以下条件成立,则函数f投射 如果f(G1,. ,G k)M,这是一个很好的例子。例4.5设f为关系→,f为非决定性选择操作员+。 它认为+propagat es→a。Infact,ifG→aGj,则nG+G→aaa 111a2GJ。此外,+投射→,因为如果G1+G2→M,则G1→M或1aG2→M。我们说,一个过程E正到达一个过程EJ,如果存在一个过程EJjndanacthaE→a EJJ和EJJreach cchesEJ.定理4.6(投影-传播复合)设f:Ek−→Ebeaparalfunctionalpro jectionp r oj c ting→h和正可达关系,传播−−·。 则W(l,−−·)相对于f是合成的。证据 假设k= 2不是限制性的。设E,F∈W(εl,−−·). 我们必须证明f(E,F)∈W(l,−−·)。如果f(E,F)达到M,则可能有两种情况• Mf(E,F);• f(E,F)正到达M。首先,我们必须证明,如果f(E,F)→hMJ,则f(E,F)−−·MJ J且MJJ≠lMJ. 如果f(E,F)→hMJ,则如果p(E,F)→h,则不严格,assumethatE→hMJ. SinceE∈W(nl,−−·),通过定义,E−−·MJJ和MJJlMJ.从f传播−−·的事实,我们得到f(E,F)−−·MJJ,也就是说,论文在第二种情况下,由于f投射了正的可达性关系,我们可以安全地假设E到达M。由于E∈ W(l,−−·)且E到达M,我们立即得到命题。 Q4.1关于代数算子的复合性下面的结果是定理4.3的一个直接结果,因为它处理的所有算子都是R→和可达关系。142A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154H推论4.7(限制,重命名,平行,定义)考虑一类解旋过程W(n,−−·)。• 让我们来看看。如果函数restv:W(l,−−·) −→ E定义为restv(E)=E\v保持−−·和l,则W(l,−−·)关于v-限制是合成的;• 设g为重命名。如果函数ren g:W(l,−−·)−→ E定义为ren g(E)=E[g]保持−−·和l,则W(l,−−·)关于g-重命名是合成的;• 如果函数par:W(nl,−−·)2−→ E定义为par(E,F)=E|F保持−·和l,则W(l,−−·)相对于平行合成是合成的|;• 如果定义f:W(l,−−·)−→E的函数定义为f(E)=Z,其中Zd=efE,保持−−·和l,则W(l,−−·)相对于常数定义d=ef是合成的。下面的结果是定理4.6的一个推论,因为非决定性选择算子投射→和正的可达关系。推论4.8(非决定性选择)设W(n,−−·)是一个展开的过程类。如果函数sum:W(l,−−·)2−→E定义为sum(E,F)= E + F传播−−·,则W(l,−−·)与关于非确定性选择运算符+。定理4.9(低前缀)设W(n,−−·)是一个展开过程类.如果l∈L是一个低层作用,那么W(l,−−·)相对于将E映射到l.E的低前缀算子是合成的。证据 我们必须证明,如果E ∈ W(<$l,−−·)且l ∈ L,则l.E ∈ W(<$l,−−·)。 如果l.E达到EJ,则可能有两种情况:• Ejl.E;•EJ ∈ Reach(E).在第一种情况下,EJ不能执行任何高层次的动作,因此我们没有什么要证明的。在第二种情况下,通过假设E∈ W(εl,−−·),我们可以得到这个结果。Q复制操作符需要一个ad-hoc定理,因为它不会重新定义。选择s→h 和可达性关系。事实上,如果!E到达EJ,这不对应于E到达EJJ和Ej!EJJ。尤其是,如果!E到达Ej,我们可以证明EJ具有E 1 的形式|......这是什么? |E n|!在那里所有的Ei下面的定理允许我们利用这种形式A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154143KK一11N可达性关系的定理4.10(复制)设W(n,−−·)是解旋过程类。如果它认为,(1) - -·包含在可达性关系中,即,如果E −−·F,则E达到F、(2) 对于每个F∈W(n,−−·)且k≥0,函数fF:W(n,−−·)k−→ E定义为fF(E1,.,E k)= E1|......这是什么?|!|! F保存玉米,(3) 对于每个k ≥ 0,函数g k:Ek −→ E使得g k(E1,.,E k)=E1|......这是什么?|E kpreserves −−·,(4) 如果F −−·FJ,则!F−−·FJ|!F、则W(n-1,--·)相对于复制算子是合成的!.证据 首先,我们要证明下面的说法。权利要求1.如果!F到达FJ,则存在n≥ 0和F1,…,F n,使得F到达F i,对于i = 1,.,n和FJ<$F1|F2|......这是什么? |F n|!F.Since!FreachesFJ,theeexistst∈Actsuchtat!F→t通过对t的长度ln的归纳。FJ.我们继续如果ln= 0,则FJ= 0!因此,我们有n= 0的命题。让我们假设我们已经证明了所有ln≤m的命题。让ln=m+1。这意味着存在FJJTJ这样!F→FJJ,tJ具有长度m,andFJJ→aFJ. 通过归纳假设,存在n≥ 0和F,…、F1N使得F到达F i,其中i = 1,...,n和FJJ<$F1|F2|......这是什么?|!|! F. 如果动作a由一个FireachesFandF→a FJ和FJ<$FJ|F|.. . . . . 你 好 。 . |F|!F. 同样,我们也得到了他1 112n如果a=τ,则是两个Fi之间的同步。 如果操作a由!F应用复制的第一规则,则F→Fn+1且FJ<$F1|F2|.. . . . . 你 好 。 . |Fn|Fn+1|!F. 类似地,我们在电子邮件中处理这些问题两种情况,即如果a由!F应用复制的第二个规则,或者如果a是一个FiF.现在我们必须证明,如果F∈W(n-1,--·),那么!F∈W(l,−−·),即,如果!FreachFJandFJ→hG,thennFj−−·GJwhichhGj<$lG.如果!F到达FJ,根据权利要求1,我们得到FJ具有F1的形式|......这是什么?|!|! F.如果n=0,则n为Fj!F. 我f!F→hG,thenF→hGJJ和GGJJ|!F. 以来F ∈ W(<$l,−−·),我们有F−−·K和K<$lGJJ。 根据假设(4),!F−−·K|!F. 此外,通过假设(1),我们有K∈W(n-1,--·),因此,根据假设(2),f F保持kl,我们得到K|!FlGJJ|!F.如果n>0,则nFJ<$F|.. . . . . 你 好 。 . |F|!F. IfFJ→hG,则可能有两种情况:144A. Bossi等/ Electronic Notes in Theoretical Computer Science 99(2004)127-154n+1个KKB• 有xistsisuchchthatF→h FJ和GF|.... . . 你 好 。 . |FJ|.... . . 你好 。 . |F|! F;ii1in• F→hFJJ和G F1|......这是什么? |F n|F JJ|!F.在第一种情况下,由于F∈W(nl,−−·)到达Fi,我们有Fi−−·K和K·K·F·J一起。因为,通过方程es(3)和d(2),gn+1preserves−−·和fFI n我们得到FJ−−·GJ<$F1|......这是什么?|......这是什么?|... |!|! F和Gj.在第二种情况下,由于F∈ W(<$l,−−·),F−−·K,其中K<$lFJJ。因此,通过po s是(4),我们得到了它!F−−·K|!F.因为,根据公式(3),gn+1保持−−·我们有F J−−·GJ<$F1|......这是什么? |F n|K|!F. 根据假设(1)我们得到K∈W(n,−−·),因此我们可以利用fF保持Ql得到GJlG.Q我们现在准备将我们的一般结果应用于安
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- WebLogic集群配置与管理实战指南
- AIX5.3上安装Weblogic 9.2详细步骤
- 面向对象编程模拟试题详解与解析
- Flex+FMS2.0中文教程:开发流媒体应用的实践指南
- PID调节深入解析:从入门到精通
- 数字水印技术:保护版权的新防线
- 8位数码管显示24小时制数字电子钟程序设计
- Mhdd免费版详细使用教程:硬盘检测与坏道屏蔽
- 操作系统期末复习指南:进程、线程与系统调用详解
- Cognos8性能优化指南:软件参数与报表设计调优
- Cognos8开发入门:从Transformer到ReportStudio
- Cisco 6509交换机配置全面指南
- C#入门:XML基础教程与实例解析
- Matlab振动分析详解:从单自由度到6自由度模型
- Eclipse JDT中的ASTParser详解与核心类介绍
- Java程序员必备资源网站大全
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功